Step | Hyp | Ref
| Expression |
1 | | brdomi 6253 |
. 2
⊢ (𝐴 ≼ 𝐵 → ∃𝑓 𝑓:𝐴–1-1→𝐵) |
2 | | f1f 5112 |
. . . . . . . 8
⊢ (𝑓:𝐴–1-1→𝐵 → 𝑓:𝐴⟶𝐵) |
3 | | ffvelrn 5321 |
. . . . . . . . 9
⊢ ((𝑓:𝐴⟶𝐵 ∧ ∪ ran
{𝑥} ∈ 𝐴) → (𝑓‘∪ ran
{𝑥}) ∈ 𝐵) |
4 | 3 | ex 113 |
. . . . . . . 8
⊢ (𝑓:𝐴⟶𝐵 → (∪ ran
{𝑥} ∈ 𝐴 → (𝑓‘∪ ran
{𝑥}) ∈ 𝐵)) |
5 | 2, 4 | syl 14 |
. . . . . . 7
⊢ (𝑓:𝐴–1-1→𝐵 → (∪ ran
{𝑥} ∈ 𝐴 → (𝑓‘∪ ran
{𝑥}) ∈ 𝐵)) |
6 | 5 | anim2d 330 |
. . . . . 6
⊢ (𝑓:𝐴–1-1→𝐵 → ((∪ dom
{𝑥} ∈ 𝐶 ∧ ∪ ran {𝑥} ∈ 𝐴) → (∪ dom
{𝑥} ∈ 𝐶 ∧ (𝑓‘∪ ran
{𝑥}) ∈ 𝐵))) |
7 | 6 | adantld 272 |
. . . . 5
⊢ (𝑓:𝐴–1-1→𝐵 → ((𝑥 = 〈∪ dom
{𝑥}, ∪ ran {𝑥}〉 ∧ (∪
dom {𝑥} ∈ 𝐶 ∧ ∪ ran {𝑥} ∈ 𝐴)) → (∪ dom
{𝑥} ∈ 𝐶 ∧ (𝑓‘∪ ran
{𝑥}) ∈ 𝐵))) |
8 | | elxp4 4828 |
. . . . 5
⊢ (𝑥 ∈ (𝐶 × 𝐴) ↔ (𝑥 = 〈∪ dom
{𝑥}, ∪ ran {𝑥}〉 ∧ (∪
dom {𝑥} ∈ 𝐶 ∧ ∪ ran {𝑥} ∈ 𝐴))) |
9 | | opelxp 4392 |
. . . . 5
⊢
(〈∪ dom {𝑥}, (𝑓‘∪ ran
{𝑥})〉 ∈ (𝐶 × 𝐵) ↔ (∪ dom
{𝑥} ∈ 𝐶 ∧ (𝑓‘∪ ran
{𝑥}) ∈ 𝐵)) |
10 | 7, 8, 9 | 3imtr4g 203 |
. . . 4
⊢ (𝑓:𝐴–1-1→𝐵 → (𝑥 ∈ (𝐶 × 𝐴) → 〈∪
dom {𝑥}, (𝑓‘∪ ran {𝑥})〉 ∈ (𝐶 × 𝐵))) |
11 | 10 | adantl 271 |
. . 3
⊢ ((𝐴 ≼ 𝐵 ∧ 𝑓:𝐴–1-1→𝐵) → (𝑥 ∈ (𝐶 × 𝐴) → 〈∪
dom {𝑥}, (𝑓‘∪ ran {𝑥})〉 ∈ (𝐶 × 𝐵))) |
12 | | elxp2 4381 |
. . . . . 6
⊢ (𝑥 ∈ (𝐶 × 𝐴) ↔ ∃𝑧 ∈ 𝐶 ∃𝑤 ∈ 𝐴 𝑥 = 〈𝑧, 𝑤〉) |
13 | | elxp2 4381 |
. . . . . 6
⊢ (𝑦 ∈ (𝐶 × 𝐴) ↔ ∃𝑣 ∈ 𝐶 ∃𝑢 ∈ 𝐴 𝑦 = 〈𝑣, 𝑢〉) |
14 | | vex 2604 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑧 ∈ V |
15 | | vex 2604 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑓 ∈ V |
16 | | vex 2604 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑤 ∈ V |
17 | 15, 16 | fvex 5215 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓‘𝑤) ∈ V |
18 | 14, 17 | opth 3992 |
. . . . . . . . . . . . . . . . 17
⊢
(〈𝑧, (𝑓‘𝑤)〉 = 〈𝑣, (𝑓‘𝑢)〉 ↔ (𝑧 = 𝑣 ∧ (𝑓‘𝑤) = (𝑓‘𝑢))) |
19 | | f1fveq 5432 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓:𝐴–1-1→𝐵 ∧ (𝑤 ∈ 𝐴 ∧ 𝑢 ∈ 𝐴)) → ((𝑓‘𝑤) = (𝑓‘𝑢) ↔ 𝑤 = 𝑢)) |
20 | 19 | ancoms 264 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑤 ∈ 𝐴 ∧ 𝑢 ∈ 𝐴) ∧ 𝑓:𝐴–1-1→𝐵) → ((𝑓‘𝑤) = (𝑓‘𝑢) ↔ 𝑤 = 𝑢)) |
21 | 20 | anbi2d 451 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑤 ∈ 𝐴 ∧ 𝑢 ∈ 𝐴) ∧ 𝑓:𝐴–1-1→𝐵) → ((𝑧 = 𝑣 ∧ (𝑓‘𝑤) = (𝑓‘𝑢)) ↔ (𝑧 = 𝑣 ∧ 𝑤 = 𝑢))) |
22 | 18, 21 | syl5bb 190 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑤 ∈ 𝐴 ∧ 𝑢 ∈ 𝐴) ∧ 𝑓:𝐴–1-1→𝐵) → (〈𝑧, (𝑓‘𝑤)〉 = 〈𝑣, (𝑓‘𝑢)〉 ↔ (𝑧 = 𝑣 ∧ 𝑤 = 𝑢))) |
23 | 22 | ex 113 |
. . . . . . . . . . . . . . 15
⊢ ((𝑤 ∈ 𝐴 ∧ 𝑢 ∈ 𝐴) → (𝑓:𝐴–1-1→𝐵 → (〈𝑧, (𝑓‘𝑤)〉 = 〈𝑣, (𝑓‘𝑢)〉 ↔ (𝑧 = 𝑣 ∧ 𝑤 = 𝑢)))) |
24 | 23 | ad2ant2l 491 |
. . . . . . . . . . . . . 14
⊢ (((𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐴) ∧ (𝑣 ∈ 𝐶 ∧ 𝑢 ∈ 𝐴)) → (𝑓:𝐴–1-1→𝐵 → (〈𝑧, (𝑓‘𝑤)〉 = 〈𝑣, (𝑓‘𝑢)〉 ↔ (𝑧 = 𝑣 ∧ 𝑤 = 𝑢)))) |
25 | 24 | imp 122 |
. . . . . . . . . . . . 13
⊢ ((((𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐴) ∧ (𝑣 ∈ 𝐶 ∧ 𝑢 ∈ 𝐴)) ∧ 𝑓:𝐴–1-1→𝐵) → (〈𝑧, (𝑓‘𝑤)〉 = 〈𝑣, (𝑓‘𝑢)〉 ↔ (𝑧 = 𝑣 ∧ 𝑤 = 𝑢))) |
26 | 25 | adantlr 460 |
. . . . . . . . . . . 12
⊢
(((((𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐴) ∧ (𝑣 ∈ 𝐶 ∧ 𝑢 ∈ 𝐴)) ∧ (𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉)) ∧ 𝑓:𝐴–1-1→𝐵) → (〈𝑧, (𝑓‘𝑤)〉 = 〈𝑣, (𝑓‘𝑢)〉 ↔ (𝑧 = 𝑣 ∧ 𝑤 = 𝑢))) |
27 | | sneq 3409 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 〈𝑧, 𝑤〉 → {𝑥} = {〈𝑧, 𝑤〉}) |
28 | 27 | dmeqd 4555 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 〈𝑧, 𝑤〉 → dom {𝑥} = dom {〈𝑧, 𝑤〉}) |
29 | 28 | unieqd 3612 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 〈𝑧, 𝑤〉 → ∪
dom {𝑥} = ∪ dom {〈𝑧, 𝑤〉}) |
30 | 14, 16 | op1sta 4822 |
. . . . . . . . . . . . . . . 16
⊢ ∪ dom {〈𝑧, 𝑤〉} = 𝑧 |
31 | 29, 30 | syl6eq 2129 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 〈𝑧, 𝑤〉 → ∪
dom {𝑥} = 𝑧) |
32 | 27 | rneqd 4581 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 〈𝑧, 𝑤〉 → ran {𝑥} = ran {〈𝑧, 𝑤〉}) |
33 | 32 | unieqd 3612 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 〈𝑧, 𝑤〉 → ∪
ran {𝑥} = ∪ ran {〈𝑧, 𝑤〉}) |
34 | 14, 16 | op2nda 4825 |
. . . . . . . . . . . . . . . . 17
⊢ ∪ ran {〈𝑧, 𝑤〉} = 𝑤 |
35 | 33, 34 | syl6eq 2129 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 〈𝑧, 𝑤〉 → ∪
ran {𝑥} = 𝑤) |
36 | 35 | fveq2d 5202 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 〈𝑧, 𝑤〉 → (𝑓‘∪ ran
{𝑥}) = (𝑓‘𝑤)) |
37 | 31, 36 | opeq12d 3578 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 〈𝑧, 𝑤〉 → 〈∪ dom {𝑥}, (𝑓‘∪ ran
{𝑥})〉 = 〈𝑧, (𝑓‘𝑤)〉) |
38 | | sneq 3409 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = 〈𝑣, 𝑢〉 → {𝑦} = {〈𝑣, 𝑢〉}) |
39 | 38 | dmeqd 4555 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 〈𝑣, 𝑢〉 → dom {𝑦} = dom {〈𝑣, 𝑢〉}) |
40 | 39 | unieqd 3612 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 〈𝑣, 𝑢〉 → ∪
dom {𝑦} = ∪ dom {〈𝑣, 𝑢〉}) |
41 | | vex 2604 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑣 ∈ V |
42 | | vex 2604 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑢 ∈ V |
43 | 41, 42 | op1sta 4822 |
. . . . . . . . . . . . . . . 16
⊢ ∪ dom {〈𝑣, 𝑢〉} = 𝑣 |
44 | 40, 43 | syl6eq 2129 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 〈𝑣, 𝑢〉 → ∪
dom {𝑦} = 𝑣) |
45 | 38 | rneqd 4581 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = 〈𝑣, 𝑢〉 → ran {𝑦} = ran {〈𝑣, 𝑢〉}) |
46 | 45 | unieqd 3612 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 〈𝑣, 𝑢〉 → ∪
ran {𝑦} = ∪ ran {〈𝑣, 𝑢〉}) |
47 | 41, 42 | op2nda 4825 |
. . . . . . . . . . . . . . . . 17
⊢ ∪ ran {〈𝑣, 𝑢〉} = 𝑢 |
48 | 46, 47 | syl6eq 2129 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 〈𝑣, 𝑢〉 → ∪
ran {𝑦} = 𝑢) |
49 | 48 | fveq2d 5202 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 〈𝑣, 𝑢〉 → (𝑓‘∪ ran
{𝑦}) = (𝑓‘𝑢)) |
50 | 44, 49 | opeq12d 3578 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 〈𝑣, 𝑢〉 → 〈∪ dom {𝑦}, (𝑓‘∪ ran
{𝑦})〉 = 〈𝑣, (𝑓‘𝑢)〉) |
51 | 37, 50 | eqeqan12d 2096 |
. . . . . . . . . . . . 13
⊢ ((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) → (〈∪ dom {𝑥}, (𝑓‘∪ ran
{𝑥})〉 = 〈∪ dom {𝑦}, (𝑓‘∪ ran
{𝑦})〉 ↔
〈𝑧, (𝑓‘𝑤)〉 = 〈𝑣, (𝑓‘𝑢)〉)) |
52 | 51 | ad2antlr 472 |
. . . . . . . . . . . 12
⊢
(((((𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐴) ∧ (𝑣 ∈ 𝐶 ∧ 𝑢 ∈ 𝐴)) ∧ (𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉)) ∧ 𝑓:𝐴–1-1→𝐵) → (〈∪
dom {𝑥}, (𝑓‘∪ ran {𝑥})〉 = 〈∪
dom {𝑦}, (𝑓‘∪ ran {𝑦})〉 ↔ 〈𝑧, (𝑓‘𝑤)〉 = 〈𝑣, (𝑓‘𝑢)〉)) |
53 | | eqeq12 2093 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) → (𝑥 = 𝑦 ↔ 〈𝑧, 𝑤〉 = 〈𝑣, 𝑢〉)) |
54 | 14, 16 | opth 3992 |
. . . . . . . . . . . . . 14
⊢
(〈𝑧, 𝑤〉 = 〈𝑣, 𝑢〉 ↔ (𝑧 = 𝑣 ∧ 𝑤 = 𝑢)) |
55 | 53, 54 | syl6bb 194 |
. . . . . . . . . . . . 13
⊢ ((𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉) → (𝑥 = 𝑦 ↔ (𝑧 = 𝑣 ∧ 𝑤 = 𝑢))) |
56 | 55 | ad2antlr 472 |
. . . . . . . . . . . 12
⊢
(((((𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐴) ∧ (𝑣 ∈ 𝐶 ∧ 𝑢 ∈ 𝐴)) ∧ (𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉)) ∧ 𝑓:𝐴–1-1→𝐵) → (𝑥 = 𝑦 ↔ (𝑧 = 𝑣 ∧ 𝑤 = 𝑢))) |
57 | 26, 52, 56 | 3bitr4d 218 |
. . . . . . . . . . 11
⊢
(((((𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐴) ∧ (𝑣 ∈ 𝐶 ∧ 𝑢 ∈ 𝐴)) ∧ (𝑥 = 〈𝑧, 𝑤〉 ∧ 𝑦 = 〈𝑣, 𝑢〉)) ∧ 𝑓:𝐴–1-1→𝐵) → (〈∪
dom {𝑥}, (𝑓‘∪ ran {𝑥})〉 = 〈∪
dom {𝑦}, (𝑓‘∪ ran {𝑦})〉 ↔ 𝑥 = 𝑦)) |
58 | 57 | exp53 369 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐴) → ((𝑣 ∈ 𝐶 ∧ 𝑢 ∈ 𝐴) → (𝑥 = 〈𝑧, 𝑤〉 → (𝑦 = 〈𝑣, 𝑢〉 → (𝑓:𝐴–1-1→𝐵 → (〈∪
dom {𝑥}, (𝑓‘∪ ran {𝑥})〉 = 〈∪
dom {𝑦}, (𝑓‘∪ ran {𝑦})〉 ↔ 𝑥 = 𝑦)))))) |
59 | 58 | com23 77 |
. . . . . . . . 9
⊢ ((𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐴) → (𝑥 = 〈𝑧, 𝑤〉 → ((𝑣 ∈ 𝐶 ∧ 𝑢 ∈ 𝐴) → (𝑦 = 〈𝑣, 𝑢〉 → (𝑓:𝐴–1-1→𝐵 → (〈∪
dom {𝑥}, (𝑓‘∪ ran {𝑥})〉 = 〈∪
dom {𝑦}, (𝑓‘∪ ran {𝑦})〉 ↔ 𝑥 = 𝑦)))))) |
60 | 59 | rexlimivv 2482 |
. . . . . . . 8
⊢
(∃𝑧 ∈
𝐶 ∃𝑤 ∈ 𝐴 𝑥 = 〈𝑧, 𝑤〉 → ((𝑣 ∈ 𝐶 ∧ 𝑢 ∈ 𝐴) → (𝑦 = 〈𝑣, 𝑢〉 → (𝑓:𝐴–1-1→𝐵 → (〈∪
dom {𝑥}, (𝑓‘∪ ran {𝑥})〉 = 〈∪
dom {𝑦}, (𝑓‘∪ ran {𝑦})〉 ↔ 𝑥 = 𝑦))))) |
61 | 60 | rexlimdvv 2483 |
. . . . . . 7
⊢
(∃𝑧 ∈
𝐶 ∃𝑤 ∈ 𝐴 𝑥 = 〈𝑧, 𝑤〉 → (∃𝑣 ∈ 𝐶 ∃𝑢 ∈ 𝐴 𝑦 = 〈𝑣, 𝑢〉 → (𝑓:𝐴–1-1→𝐵 → (〈∪
dom {𝑥}, (𝑓‘∪ ran {𝑥})〉 = 〈∪
dom {𝑦}, (𝑓‘∪ ran {𝑦})〉 ↔ 𝑥 = 𝑦)))) |
62 | 61 | imp 122 |
. . . . . 6
⊢
((∃𝑧 ∈
𝐶 ∃𝑤 ∈ 𝐴 𝑥 = 〈𝑧, 𝑤〉 ∧ ∃𝑣 ∈ 𝐶 ∃𝑢 ∈ 𝐴 𝑦 = 〈𝑣, 𝑢〉) → (𝑓:𝐴–1-1→𝐵 → (〈∪
dom {𝑥}, (𝑓‘∪ ran {𝑥})〉 = 〈∪
dom {𝑦}, (𝑓‘∪ ran {𝑦})〉 ↔ 𝑥 = 𝑦))) |
63 | 12, 13, 62 | syl2anb 285 |
. . . . 5
⊢ ((𝑥 ∈ (𝐶 × 𝐴) ∧ 𝑦 ∈ (𝐶 × 𝐴)) → (𝑓:𝐴–1-1→𝐵 → (〈∪
dom {𝑥}, (𝑓‘∪ ran {𝑥})〉 = 〈∪
dom {𝑦}, (𝑓‘∪ ran {𝑦})〉 ↔ 𝑥 = 𝑦))) |
64 | 63 | com12 30 |
. . . 4
⊢ (𝑓:𝐴–1-1→𝐵 → ((𝑥 ∈ (𝐶 × 𝐴) ∧ 𝑦 ∈ (𝐶 × 𝐴)) → (〈∪ dom {𝑥}, (𝑓‘∪ ran
{𝑥})〉 = 〈∪ dom {𝑦}, (𝑓‘∪ ran
{𝑦})〉 ↔ 𝑥 = 𝑦))) |
65 | 64 | adantl 271 |
. . 3
⊢ ((𝐴 ≼ 𝐵 ∧ 𝑓:𝐴–1-1→𝐵) → ((𝑥 ∈ (𝐶 × 𝐴) ∧ 𝑦 ∈ (𝐶 × 𝐴)) → (〈∪ dom {𝑥}, (𝑓‘∪ ran
{𝑥})〉 = 〈∪ dom {𝑦}, (𝑓‘∪ ran
{𝑦})〉 ↔ 𝑥 = 𝑦))) |
66 | | xpdom.2 |
. . . . 5
⊢ 𝐶 ∈ V |
67 | | reldom 6249 |
. . . . . 6
⊢ Rel
≼ |
68 | 67 | brrelexi 4402 |
. . . . 5
⊢ (𝐴 ≼ 𝐵 → 𝐴 ∈ V) |
69 | | xpexg 4470 |
. . . . 5
⊢ ((𝐶 ∈ V ∧ 𝐴 ∈ V) → (𝐶 × 𝐴) ∈ V) |
70 | 66, 68, 69 | sylancr 405 |
. . . 4
⊢ (𝐴 ≼ 𝐵 → (𝐶 × 𝐴) ∈ V) |
71 | 70 | adantr 270 |
. . 3
⊢ ((𝐴 ≼ 𝐵 ∧ 𝑓:𝐴–1-1→𝐵) → (𝐶 × 𝐴) ∈ V) |
72 | 67 | brrelex2i 4403 |
. . . . 5
⊢ (𝐴 ≼ 𝐵 → 𝐵 ∈ V) |
73 | | xpexg 4470 |
. . . . 5
⊢ ((𝐶 ∈ V ∧ 𝐵 ∈ V) → (𝐶 × 𝐵) ∈ V) |
74 | 66, 72, 73 | sylancr 405 |
. . . 4
⊢ (𝐴 ≼ 𝐵 → (𝐶 × 𝐵) ∈ V) |
75 | 74 | adantr 270 |
. . 3
⊢ ((𝐴 ≼ 𝐵 ∧ 𝑓:𝐴–1-1→𝐵) → (𝐶 × 𝐵) ∈ V) |
76 | 11, 65, 71, 75 | dom3d 6277 |
. 2
⊢ ((𝐴 ≼ 𝐵 ∧ 𝑓:𝐴–1-1→𝐵) → (𝐶 × 𝐴) ≼ (𝐶 × 𝐵)) |
77 | 1, 76 | exlimddv 1819 |
1
⊢ (𝐴 ≼ 𝐵 → (𝐶 × 𝐴) ≼ (𝐶 × 𝐵)) |