Step | Hyp | Ref
| Expression |
1 | | brdomi 8954 |
. 2
⊢ (𝐴 ≼ 𝐵 → ∃𝑓 𝑓:𝐴–1-1→𝐵) |
2 | | f1f 6788 |
. . . . . . . 8
⊢ (𝑓:𝐴–1-1→𝐵 → 𝑓:𝐴⟶𝐵) |
3 | | ffvelcdm 7084 |
. . . . . . . . 9
⊢ ((𝑓:𝐴⟶𝐵 ∧ ∪ ran
{𝑥} ∈ 𝐴) → (𝑓‘∪ ran
{𝑥}) ∈ 𝐵) |
4 | 3 | ex 414 |
. . . . . . . 8
⊢ (𝑓:𝐴⟶𝐵 → (∪ ran
{𝑥} ∈ 𝐴 → (𝑓‘∪ ran
{𝑥}) ∈ 𝐵)) |
5 | 2, 4 | syl 17 |
. . . . . . 7
⊢ (𝑓:𝐴–1-1→𝐵 → (∪ ran
{𝑥} ∈ 𝐴 → (𝑓‘∪ ran
{𝑥}) ∈ 𝐵)) |
6 | 5 | anim2d 613 |
. . . . . 6
⊢ (𝑓:𝐴–1-1→𝐵 → ((∪ dom
{𝑥} ∈ 𝐶 ∧ ∪ ran {𝑥} ∈ 𝐴) → (∪ dom
{𝑥} ∈ 𝐶 ∧ (𝑓‘∪ ran
{𝑥}) ∈ 𝐵))) |
7 | 6 | adantld 492 |
. . . . 5
⊢ (𝑓:𝐴–1-1→𝐵 → ((𝑥 = ⟨∪ dom
{𝑥}, ∪ ran {𝑥}⟩ ∧ (∪
dom {𝑥} ∈ 𝐶 ∧ ∪ ran {𝑥} ∈ 𝐴)) → (∪ dom
{𝑥} ∈ 𝐶 ∧ (𝑓‘∪ ran
{𝑥}) ∈ 𝐵))) |
8 | | elxp4 7913 |
. . . . 5
⊢ (𝑥 ∈ (𝐶 × 𝐴) ↔ (𝑥 = ⟨∪ dom
{𝑥}, ∪ ran {𝑥}⟩ ∧ (∪
dom {𝑥} ∈ 𝐶 ∧ ∪ ran {𝑥} ∈ 𝐴))) |
9 | | opelxp 5713 |
. . . . 5
⊢
(⟨∪ dom {𝑥}, (𝑓‘∪ ran
{𝑥})⟩ ∈ (𝐶 × 𝐵) ↔ (∪ dom
{𝑥} ∈ 𝐶 ∧ (𝑓‘∪ ran
{𝑥}) ∈ 𝐵)) |
10 | 7, 8, 9 | 3imtr4g 296 |
. . . 4
⊢ (𝑓:𝐴–1-1→𝐵 → (𝑥 ∈ (𝐶 × 𝐴) → ⟨∪
dom {𝑥}, (𝑓‘∪ ran {𝑥})⟩ ∈ (𝐶 × 𝐵))) |
11 | 10 | adantl 483 |
. . 3
⊢ ((𝐴 ≼ 𝐵 ∧ 𝑓:𝐴–1-1→𝐵) → (𝑥 ∈ (𝐶 × 𝐴) → ⟨∪
dom {𝑥}, (𝑓‘∪ ran {𝑥})⟩ ∈ (𝐶 × 𝐵))) |
12 | | elxp2 5701 |
. . . . . 6
⊢ (𝑥 ∈ (𝐶 × 𝐴) ↔ ∃𝑧 ∈ 𝐶 ∃𝑤 ∈ 𝐴 𝑥 = ⟨𝑧, 𝑤⟩) |
13 | | elxp2 5701 |
. . . . . 6
⊢ (𝑦 ∈ (𝐶 × 𝐴) ↔ ∃𝑣 ∈ 𝐶 ∃𝑢 ∈ 𝐴 𝑦 = ⟨𝑣, 𝑢⟩) |
14 | | vex 3479 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑧 ∈ V |
15 | | fvex 6905 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓‘𝑤) ∈ V |
16 | 14, 15 | opth 5477 |
. . . . . . . . . . . . . . . . 17
⊢
(⟨𝑧, (𝑓‘𝑤)⟩ = ⟨𝑣, (𝑓‘𝑢)⟩ ↔ (𝑧 = 𝑣 ∧ (𝑓‘𝑤) = (𝑓‘𝑢))) |
17 | | f1fveq 7261 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓:𝐴–1-1→𝐵 ∧ (𝑤 ∈ 𝐴 ∧ 𝑢 ∈ 𝐴)) → ((𝑓‘𝑤) = (𝑓‘𝑢) ↔ 𝑤 = 𝑢)) |
18 | 17 | ancoms 460 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑤 ∈ 𝐴 ∧ 𝑢 ∈ 𝐴) ∧ 𝑓:𝐴–1-1→𝐵) → ((𝑓‘𝑤) = (𝑓‘𝑢) ↔ 𝑤 = 𝑢)) |
19 | 18 | anbi2d 630 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑤 ∈ 𝐴 ∧ 𝑢 ∈ 𝐴) ∧ 𝑓:𝐴–1-1→𝐵) → ((𝑧 = 𝑣 ∧ (𝑓‘𝑤) = (𝑓‘𝑢)) ↔ (𝑧 = 𝑣 ∧ 𝑤 = 𝑢))) |
20 | 16, 19 | bitrid 283 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑤 ∈ 𝐴 ∧ 𝑢 ∈ 𝐴) ∧ 𝑓:𝐴–1-1→𝐵) → (⟨𝑧, (𝑓‘𝑤)⟩ = ⟨𝑣, (𝑓‘𝑢)⟩ ↔ (𝑧 = 𝑣 ∧ 𝑤 = 𝑢))) |
21 | 20 | ex 414 |
. . . . . . . . . . . . . . 15
⊢ ((𝑤 ∈ 𝐴 ∧ 𝑢 ∈ 𝐴) → (𝑓:𝐴–1-1→𝐵 → (⟨𝑧, (𝑓‘𝑤)⟩ = ⟨𝑣, (𝑓‘𝑢)⟩ ↔ (𝑧 = 𝑣 ∧ 𝑤 = 𝑢)))) |
22 | 21 | ad2ant2l 745 |
. . . . . . . . . . . . . 14
⊢ (((𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐴) ∧ (𝑣 ∈ 𝐶 ∧ 𝑢 ∈ 𝐴)) → (𝑓:𝐴–1-1→𝐵 → (⟨𝑧, (𝑓‘𝑤)⟩ = ⟨𝑣, (𝑓‘𝑢)⟩ ↔ (𝑧 = 𝑣 ∧ 𝑤 = 𝑢)))) |
23 | 22 | imp 408 |
. . . . . . . . . . . . 13
⊢ ((((𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐴) ∧ (𝑣 ∈ 𝐶 ∧ 𝑢 ∈ 𝐴)) ∧ 𝑓:𝐴–1-1→𝐵) → (⟨𝑧, (𝑓‘𝑤)⟩ = ⟨𝑣, (𝑓‘𝑢)⟩ ↔ (𝑧 = 𝑣 ∧ 𝑤 = 𝑢))) |
24 | 23 | adantlr 714 |
. . . . . . . . . . . 12
⊢
(((((𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐴) ∧ (𝑣 ∈ 𝐶 ∧ 𝑢 ∈ 𝐴)) ∧ (𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩)) ∧ 𝑓:𝐴–1-1→𝐵) → (⟨𝑧, (𝑓‘𝑤)⟩ = ⟨𝑣, (𝑓‘𝑢)⟩ ↔ (𝑧 = 𝑣 ∧ 𝑤 = 𝑢))) |
25 | | sneq 4639 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = ⟨𝑧, 𝑤⟩ → {𝑥} = {⟨𝑧, 𝑤⟩}) |
26 | 25 | dmeqd 5906 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = ⟨𝑧, 𝑤⟩ → dom {𝑥} = dom {⟨𝑧, 𝑤⟩}) |
27 | 26 | unieqd 4923 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = ⟨𝑧, 𝑤⟩ → ∪
dom {𝑥} = ∪ dom {⟨𝑧, 𝑤⟩}) |
28 | | vex 3479 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑤 ∈ V |
29 | 14, 28 | op1sta 6225 |
. . . . . . . . . . . . . . . 16
⊢ ∪ dom {⟨𝑧, 𝑤⟩} = 𝑧 |
30 | 27, 29 | eqtrdi 2789 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = ⟨𝑧, 𝑤⟩ → ∪
dom {𝑥} = 𝑧) |
31 | 25 | rneqd 5938 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = ⟨𝑧, 𝑤⟩ → ran {𝑥} = ran {⟨𝑧, 𝑤⟩}) |
32 | 31 | unieqd 4923 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = ⟨𝑧, 𝑤⟩ → ∪
ran {𝑥} = ∪ ran {⟨𝑧, 𝑤⟩}) |
33 | 14, 28 | op2nda 6228 |
. . . . . . . . . . . . . . . . 17
⊢ ∪ ran {⟨𝑧, 𝑤⟩} = 𝑤 |
34 | 32, 33 | eqtrdi 2789 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = ⟨𝑧, 𝑤⟩ → ∪
ran {𝑥} = 𝑤) |
35 | 34 | fveq2d 6896 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = ⟨𝑧, 𝑤⟩ → (𝑓‘∪ ran
{𝑥}) = (𝑓‘𝑤)) |
36 | 30, 35 | opeq12d 4882 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = ⟨𝑧, 𝑤⟩ → ⟨∪ dom {𝑥}, (𝑓‘∪ ran
{𝑥})⟩ = ⟨𝑧, (𝑓‘𝑤)⟩) |
37 | | sneq 4639 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = ⟨𝑣, 𝑢⟩ → {𝑦} = {⟨𝑣, 𝑢⟩}) |
38 | 37 | dmeqd 5906 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = ⟨𝑣, 𝑢⟩ → dom {𝑦} = dom {⟨𝑣, 𝑢⟩}) |
39 | 38 | unieqd 4923 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = ⟨𝑣, 𝑢⟩ → ∪
dom {𝑦} = ∪ dom {⟨𝑣, 𝑢⟩}) |
40 | | vex 3479 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑣 ∈ V |
41 | | vex 3479 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑢 ∈ V |
42 | 40, 41 | op1sta 6225 |
. . . . . . . . . . . . . . . 16
⊢ ∪ dom {⟨𝑣, 𝑢⟩} = 𝑣 |
43 | 39, 42 | eqtrdi 2789 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = ⟨𝑣, 𝑢⟩ → ∪
dom {𝑦} = 𝑣) |
44 | 37 | rneqd 5938 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = ⟨𝑣, 𝑢⟩ → ran {𝑦} = ran {⟨𝑣, 𝑢⟩}) |
45 | 44 | unieqd 4923 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = ⟨𝑣, 𝑢⟩ → ∪
ran {𝑦} = ∪ ran {⟨𝑣, 𝑢⟩}) |
46 | 40, 41 | op2nda 6228 |
. . . . . . . . . . . . . . . . 17
⊢ ∪ ran {⟨𝑣, 𝑢⟩} = 𝑢 |
47 | 45, 46 | eqtrdi 2789 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = ⟨𝑣, 𝑢⟩ → ∪
ran {𝑦} = 𝑢) |
48 | 47 | fveq2d 6896 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = ⟨𝑣, 𝑢⟩ → (𝑓‘∪ ran
{𝑦}) = (𝑓‘𝑢)) |
49 | 43, 48 | opeq12d 4882 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = ⟨𝑣, 𝑢⟩ → ⟨∪ dom {𝑦}, (𝑓‘∪ ran
{𝑦})⟩ = ⟨𝑣, (𝑓‘𝑢)⟩) |
50 | 36, 49 | eqeqan12d 2747 |
. . . . . . . . . . . . 13
⊢ ((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) → (⟨∪ dom {𝑥}, (𝑓‘∪ ran
{𝑥})⟩ = ⟨∪ dom {𝑦}, (𝑓‘∪ ran
{𝑦})⟩ ↔
⟨𝑧, (𝑓‘𝑤)⟩ = ⟨𝑣, (𝑓‘𝑢)⟩)) |
51 | 50 | ad2antlr 726 |
. . . . . . . . . . . 12
⊢
(((((𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐴) ∧ (𝑣 ∈ 𝐶 ∧ 𝑢 ∈ 𝐴)) ∧ (𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩)) ∧ 𝑓:𝐴–1-1→𝐵) → (⟨∪
dom {𝑥}, (𝑓‘∪ ran {𝑥})⟩ = ⟨∪
dom {𝑦}, (𝑓‘∪ ran {𝑦})⟩ ↔ ⟨𝑧, (𝑓‘𝑤)⟩ = ⟨𝑣, (𝑓‘𝑢)⟩)) |
52 | | eqeq12 2750 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) → (𝑥 = 𝑦 ↔ ⟨𝑧, 𝑤⟩ = ⟨𝑣, 𝑢⟩)) |
53 | 14, 28 | opth 5477 |
. . . . . . . . . . . . . 14
⊢
(⟨𝑧, 𝑤⟩ = ⟨𝑣, 𝑢⟩ ↔ (𝑧 = 𝑣 ∧ 𝑤 = 𝑢)) |
54 | 52, 53 | bitrdi 287 |
. . . . . . . . . . . . 13
⊢ ((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) → (𝑥 = 𝑦 ↔ (𝑧 = 𝑣 ∧ 𝑤 = 𝑢))) |
55 | 54 | ad2antlr 726 |
. . . . . . . . . . . 12
⊢
(((((𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐴) ∧ (𝑣 ∈ 𝐶 ∧ 𝑢 ∈ 𝐴)) ∧ (𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩)) ∧ 𝑓:𝐴–1-1→𝐵) → (𝑥 = 𝑦 ↔ (𝑧 = 𝑣 ∧ 𝑤 = 𝑢))) |
56 | 24, 51, 55 | 3bitr4d 311 |
. . . . . . . . . . 11
⊢
(((((𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐴) ∧ (𝑣 ∈ 𝐶 ∧ 𝑢 ∈ 𝐴)) ∧ (𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩)) ∧ 𝑓:𝐴–1-1→𝐵) → (⟨∪
dom {𝑥}, (𝑓‘∪ ran {𝑥})⟩ = ⟨∪
dom {𝑦}, (𝑓‘∪ ran {𝑦})⟩ ↔ 𝑥 = 𝑦)) |
57 | 56 | exp53 449 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐴) → ((𝑣 ∈ 𝐶 ∧ 𝑢 ∈ 𝐴) → (𝑥 = ⟨𝑧, 𝑤⟩ → (𝑦 = ⟨𝑣, 𝑢⟩ → (𝑓:𝐴–1-1→𝐵 → (⟨∪
dom {𝑥}, (𝑓‘∪ ran {𝑥})⟩ = ⟨∪
dom {𝑦}, (𝑓‘∪ ran {𝑦})⟩ ↔ 𝑥 = 𝑦)))))) |
58 | 57 | com23 86 |
. . . . . . . . 9
⊢ ((𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐴) → (𝑥 = ⟨𝑧, 𝑤⟩ → ((𝑣 ∈ 𝐶 ∧ 𝑢 ∈ 𝐴) → (𝑦 = ⟨𝑣, 𝑢⟩ → (𝑓:𝐴–1-1→𝐵 → (⟨∪
dom {𝑥}, (𝑓‘∪ ran {𝑥})⟩ = ⟨∪
dom {𝑦}, (𝑓‘∪ ran {𝑦})⟩ ↔ 𝑥 = 𝑦)))))) |
59 | 58 | rexlimivv 3200 |
. . . . . . . 8
⊢
(∃𝑧 ∈
𝐶 ∃𝑤 ∈ 𝐴 𝑥 = ⟨𝑧, 𝑤⟩ → ((𝑣 ∈ 𝐶 ∧ 𝑢 ∈ 𝐴) → (𝑦 = ⟨𝑣, 𝑢⟩ → (𝑓:𝐴–1-1→𝐵 → (⟨∪
dom {𝑥}, (𝑓‘∪ ran {𝑥})⟩ = ⟨∪
dom {𝑦}, (𝑓‘∪ ran {𝑦})⟩ ↔ 𝑥 = 𝑦))))) |
60 | 59 | rexlimdvv 3211 |
. . . . . . 7
⊢
(∃𝑧 ∈
𝐶 ∃𝑤 ∈ 𝐴 𝑥 = ⟨𝑧, 𝑤⟩ → (∃𝑣 ∈ 𝐶 ∃𝑢 ∈ 𝐴 𝑦 = ⟨𝑣, 𝑢⟩ → (𝑓:𝐴–1-1→𝐵 → (⟨∪
dom {𝑥}, (𝑓‘∪ ran {𝑥})⟩ = ⟨∪
dom {𝑦}, (𝑓‘∪ ran {𝑦})⟩ ↔ 𝑥 = 𝑦)))) |
61 | 60 | imp 408 |
. . . . . 6
⊢
((∃𝑧 ∈
𝐶 ∃𝑤 ∈ 𝐴 𝑥 = ⟨𝑧, 𝑤⟩ ∧ ∃𝑣 ∈ 𝐶 ∃𝑢 ∈ 𝐴 𝑦 = ⟨𝑣, 𝑢⟩) → (𝑓:𝐴–1-1→𝐵 → (⟨∪
dom {𝑥}, (𝑓‘∪ ran {𝑥})⟩ = ⟨∪
dom {𝑦}, (𝑓‘∪ ran {𝑦})⟩ ↔ 𝑥 = 𝑦))) |
62 | 12, 13, 61 | syl2anb 599 |
. . . . 5
⊢ ((𝑥 ∈ (𝐶 × 𝐴) ∧ 𝑦 ∈ (𝐶 × 𝐴)) → (𝑓:𝐴–1-1→𝐵 → (⟨∪
dom {𝑥}, (𝑓‘∪ ran {𝑥})⟩ = ⟨∪
dom {𝑦}, (𝑓‘∪ ran {𝑦})⟩ ↔ 𝑥 = 𝑦))) |
63 | 62 | com12 32 |
. . . 4
⊢ (𝑓:𝐴–1-1→𝐵 → ((𝑥 ∈ (𝐶 × 𝐴) ∧ 𝑦 ∈ (𝐶 × 𝐴)) → (⟨∪ dom {𝑥}, (𝑓‘∪ ran
{𝑥})⟩ = ⟨∪ dom {𝑦}, (𝑓‘∪ ran
{𝑦})⟩ ↔ 𝑥 = 𝑦))) |
64 | 63 | adantl 483 |
. . 3
⊢ ((𝐴 ≼ 𝐵 ∧ 𝑓:𝐴–1-1→𝐵) → ((𝑥 ∈ (𝐶 × 𝐴) ∧ 𝑦 ∈ (𝐶 × 𝐴)) → (⟨∪ dom {𝑥}, (𝑓‘∪ ran
{𝑥})⟩ = ⟨∪ dom {𝑦}, (𝑓‘∪ ran
{𝑦})⟩ ↔ 𝑥 = 𝑦))) |
65 | | xpdom.2 |
. . . . 5
⊢ 𝐶 ∈ V |
66 | | reldom 8945 |
. . . . . 6
⊢ Rel
≼ |
67 | 66 | brrelex1i 5733 |
. . . . 5
⊢ (𝐴 ≼ 𝐵 → 𝐴 ∈ V) |
68 | | xpexg 7737 |
. . . . 5
⊢ ((𝐶 ∈ V ∧ 𝐴 ∈ V) → (𝐶 × 𝐴) ∈ V) |
69 | 65, 67, 68 | sylancr 588 |
. . . 4
⊢ (𝐴 ≼ 𝐵 → (𝐶 × 𝐴) ∈ V) |
70 | 69 | adantr 482 |
. . 3
⊢ ((𝐴 ≼ 𝐵 ∧ 𝑓:𝐴–1-1→𝐵) → (𝐶 × 𝐴) ∈ V) |
71 | 66 | brrelex2i 5734 |
. . . . 5
⊢ (𝐴 ≼ 𝐵 → 𝐵 ∈ V) |
72 | | xpexg 7737 |
. . . . 5
⊢ ((𝐶 ∈ V ∧ 𝐵 ∈ V) → (𝐶 × 𝐵) ∈ V) |
73 | 65, 71, 72 | sylancr 588 |
. . . 4
⊢ (𝐴 ≼ 𝐵 → (𝐶 × 𝐵) ∈ V) |
74 | 73 | adantr 482 |
. . 3
⊢ ((𝐴 ≼ 𝐵 ∧ 𝑓:𝐴–1-1→𝐵) → (𝐶 × 𝐵) ∈ V) |
75 | 11, 64, 70, 74 | dom3d 8990 |
. 2
⊢ ((𝐴 ≼ 𝐵 ∧ 𝑓:𝐴–1-1→𝐵) → (𝐶 × 𝐴) ≼ (𝐶 × 𝐵)) |
76 | 1, 75 | exlimddv 1939 |
1
⊢ (𝐴 ≼ 𝐵 → (𝐶 × 𝐴) ≼ (𝐶 × 𝐵)) |