Step | Hyp | Ref
| Expression |
1 | | brdomi 6748 |
. 2
⊢ (𝐴 ≼ 𝐵 → ∃𝑓 𝑓:𝐴–1-1→𝐵) |
2 | | f1f 5421 |
. . . . . . . 8
⊢ (𝑓:𝐴–1-1→𝐵 → 𝑓:𝐴⟶𝐵) |
3 | | ffvelcdm 5649 |
. . . . . . . . 9
⊢ ((𝑓:𝐴⟶𝐵 ∧ ∪ ran
{𝑥} ∈ 𝐴) → (𝑓‘∪ ran
{𝑥}) ∈ 𝐵) |
4 | 3 | ex 115 |
. . . . . . . 8
⊢ (𝑓:𝐴⟶𝐵 → (∪ ran
{𝑥} ∈ 𝐴 → (𝑓‘∪ ran
{𝑥}) ∈ 𝐵)) |
5 | 2, 4 | syl 14 |
. . . . . . 7
⊢ (𝑓:𝐴–1-1→𝐵 → (∪ ran
{𝑥} ∈ 𝐴 → (𝑓‘∪ ran
{𝑥}) ∈ 𝐵)) |
6 | 5 | anim2d 337 |
. . . . . 6
⊢ (𝑓:𝐴–1-1→𝐵 → ((∪ dom
{𝑥} ∈ 𝐶 ∧ ∪ ran {𝑥} ∈ 𝐴) → (∪ dom
{𝑥} ∈ 𝐶 ∧ (𝑓‘∪ ran
{𝑥}) ∈ 𝐵))) |
7 | 6 | adantld 278 |
. . . . 5
⊢ (𝑓:𝐴–1-1→𝐵 → ((𝑥 = ⟨∪ dom
{𝑥}, ∪ ran {𝑥}⟩ ∧ (∪
dom {𝑥} ∈ 𝐶 ∧ ∪ ran {𝑥} ∈ 𝐴)) → (∪ dom
{𝑥} ∈ 𝐶 ∧ (𝑓‘∪ ran
{𝑥}) ∈ 𝐵))) |
8 | | elxp4 5116 |
. . . . 5
⊢ (𝑥 ∈ (𝐶 × 𝐴) ↔ (𝑥 = ⟨∪ dom
{𝑥}, ∪ ran {𝑥}⟩ ∧ (∪
dom {𝑥} ∈ 𝐶 ∧ ∪ ran {𝑥} ∈ 𝐴))) |
9 | | opelxp 4656 |
. . . . 5
⊢
(⟨∪ dom {𝑥}, (𝑓‘∪ ran
{𝑥})⟩ ∈ (𝐶 × 𝐵) ↔ (∪ dom
{𝑥} ∈ 𝐶 ∧ (𝑓‘∪ ran
{𝑥}) ∈ 𝐵)) |
10 | 7, 8, 9 | 3imtr4g 205 |
. . . 4
⊢ (𝑓:𝐴–1-1→𝐵 → (𝑥 ∈ (𝐶 × 𝐴) → ⟨∪
dom {𝑥}, (𝑓‘∪ ran {𝑥})⟩ ∈ (𝐶 × 𝐵))) |
11 | 10 | adantl 277 |
. . 3
⊢ ((𝐴 ≼ 𝐵 ∧ 𝑓:𝐴–1-1→𝐵) → (𝑥 ∈ (𝐶 × 𝐴) → ⟨∪
dom {𝑥}, (𝑓‘∪ ran {𝑥})⟩ ∈ (𝐶 × 𝐵))) |
12 | | elxp2 4644 |
. . . . . 6
⊢ (𝑥 ∈ (𝐶 × 𝐴) ↔ ∃𝑧 ∈ 𝐶 ∃𝑤 ∈ 𝐴 𝑥 = ⟨𝑧, 𝑤⟩) |
13 | | elxp2 4644 |
. . . . . 6
⊢ (𝑦 ∈ (𝐶 × 𝐴) ↔ ∃𝑣 ∈ 𝐶 ∃𝑢 ∈ 𝐴 𝑦 = ⟨𝑣, 𝑢⟩) |
14 | | vex 2740 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑧 ∈ V |
15 | | vex 2740 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑓 ∈ V |
16 | | vex 2740 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑤 ∈ V |
17 | 15, 16 | fvex 5535 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓‘𝑤) ∈ V |
18 | 14, 17 | opth 4237 |
. . . . . . . . . . . . . . . . 17
⊢
(⟨𝑧, (𝑓‘𝑤)⟩ = ⟨𝑣, (𝑓‘𝑢)⟩ ↔ (𝑧 = 𝑣 ∧ (𝑓‘𝑤) = (𝑓‘𝑢))) |
19 | | f1fveq 5772 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓:𝐴–1-1→𝐵 ∧ (𝑤 ∈ 𝐴 ∧ 𝑢 ∈ 𝐴)) → ((𝑓‘𝑤) = (𝑓‘𝑢) ↔ 𝑤 = 𝑢)) |
20 | 19 | ancoms 268 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑤 ∈ 𝐴 ∧ 𝑢 ∈ 𝐴) ∧ 𝑓:𝐴–1-1→𝐵) → ((𝑓‘𝑤) = (𝑓‘𝑢) ↔ 𝑤 = 𝑢)) |
21 | 20 | anbi2d 464 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑤 ∈ 𝐴 ∧ 𝑢 ∈ 𝐴) ∧ 𝑓:𝐴–1-1→𝐵) → ((𝑧 = 𝑣 ∧ (𝑓‘𝑤) = (𝑓‘𝑢)) ↔ (𝑧 = 𝑣 ∧ 𝑤 = 𝑢))) |
22 | 18, 21 | bitrid 192 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑤 ∈ 𝐴 ∧ 𝑢 ∈ 𝐴) ∧ 𝑓:𝐴–1-1→𝐵) → (⟨𝑧, (𝑓‘𝑤)⟩ = ⟨𝑣, (𝑓‘𝑢)⟩ ↔ (𝑧 = 𝑣 ∧ 𝑤 = 𝑢))) |
23 | 22 | ex 115 |
. . . . . . . . . . . . . . 15
⊢ ((𝑤 ∈ 𝐴 ∧ 𝑢 ∈ 𝐴) → (𝑓:𝐴–1-1→𝐵 → (⟨𝑧, (𝑓‘𝑤)⟩ = ⟨𝑣, (𝑓‘𝑢)⟩ ↔ (𝑧 = 𝑣 ∧ 𝑤 = 𝑢)))) |
24 | 23 | ad2ant2l 508 |
. . . . . . . . . . . . . 14
⊢ (((𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐴) ∧ (𝑣 ∈ 𝐶 ∧ 𝑢 ∈ 𝐴)) → (𝑓:𝐴–1-1→𝐵 → (⟨𝑧, (𝑓‘𝑤)⟩ = ⟨𝑣, (𝑓‘𝑢)⟩ ↔ (𝑧 = 𝑣 ∧ 𝑤 = 𝑢)))) |
25 | 24 | imp 124 |
. . . . . . . . . . . . 13
⊢ ((((𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐴) ∧ (𝑣 ∈ 𝐶 ∧ 𝑢 ∈ 𝐴)) ∧ 𝑓:𝐴–1-1→𝐵) → (⟨𝑧, (𝑓‘𝑤)⟩ = ⟨𝑣, (𝑓‘𝑢)⟩ ↔ (𝑧 = 𝑣 ∧ 𝑤 = 𝑢))) |
26 | 25 | adantlr 477 |
. . . . . . . . . . . 12
⊢
(((((𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐴) ∧ (𝑣 ∈ 𝐶 ∧ 𝑢 ∈ 𝐴)) ∧ (𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩)) ∧ 𝑓:𝐴–1-1→𝐵) → (⟨𝑧, (𝑓‘𝑤)⟩ = ⟨𝑣, (𝑓‘𝑢)⟩ ↔ (𝑧 = 𝑣 ∧ 𝑤 = 𝑢))) |
27 | | sneq 3603 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = ⟨𝑧, 𝑤⟩ → {𝑥} = {⟨𝑧, 𝑤⟩}) |
28 | 27 | dmeqd 4829 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = ⟨𝑧, 𝑤⟩ → dom {𝑥} = dom {⟨𝑧, 𝑤⟩}) |
29 | 28 | unieqd 3820 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = ⟨𝑧, 𝑤⟩ → ∪
dom {𝑥} = ∪ dom {⟨𝑧, 𝑤⟩}) |
30 | 14, 16 | op1sta 5110 |
. . . . . . . . . . . . . . . 16
⊢ ∪ dom {⟨𝑧, 𝑤⟩} = 𝑧 |
31 | 29, 30 | eqtrdi 2226 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = ⟨𝑧, 𝑤⟩ → ∪
dom {𝑥} = 𝑧) |
32 | 27 | rneqd 4856 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = ⟨𝑧, 𝑤⟩ → ran {𝑥} = ran {⟨𝑧, 𝑤⟩}) |
33 | 32 | unieqd 3820 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = ⟨𝑧, 𝑤⟩ → ∪
ran {𝑥} = ∪ ran {⟨𝑧, 𝑤⟩}) |
34 | 14, 16 | op2nda 5113 |
. . . . . . . . . . . . . . . . 17
⊢ ∪ ran {⟨𝑧, 𝑤⟩} = 𝑤 |
35 | 33, 34 | eqtrdi 2226 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = ⟨𝑧, 𝑤⟩ → ∪
ran {𝑥} = 𝑤) |
36 | 35 | fveq2d 5519 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = ⟨𝑧, 𝑤⟩ → (𝑓‘∪ ran
{𝑥}) = (𝑓‘𝑤)) |
37 | 31, 36 | opeq12d 3786 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = ⟨𝑧, 𝑤⟩ → ⟨∪ dom {𝑥}, (𝑓‘∪ ran
{𝑥})⟩ = ⟨𝑧, (𝑓‘𝑤)⟩) |
38 | | sneq 3603 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = ⟨𝑣, 𝑢⟩ → {𝑦} = {⟨𝑣, 𝑢⟩}) |
39 | 38 | dmeqd 4829 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = ⟨𝑣, 𝑢⟩ → dom {𝑦} = dom {⟨𝑣, 𝑢⟩}) |
40 | 39 | unieqd 3820 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = ⟨𝑣, 𝑢⟩ → ∪
dom {𝑦} = ∪ dom {⟨𝑣, 𝑢⟩}) |
41 | | vex 2740 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑣 ∈ V |
42 | | vex 2740 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑢 ∈ V |
43 | 41, 42 | op1sta 5110 |
. . . . . . . . . . . . . . . 16
⊢ ∪ dom {⟨𝑣, 𝑢⟩} = 𝑣 |
44 | 40, 43 | eqtrdi 2226 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = ⟨𝑣, 𝑢⟩ → ∪
dom {𝑦} = 𝑣) |
45 | 38 | rneqd 4856 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = ⟨𝑣, 𝑢⟩ → ran {𝑦} = ran {⟨𝑣, 𝑢⟩}) |
46 | 45 | unieqd 3820 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = ⟨𝑣, 𝑢⟩ → ∪
ran {𝑦} = ∪ ran {⟨𝑣, 𝑢⟩}) |
47 | 41, 42 | op2nda 5113 |
. . . . . . . . . . . . . . . . 17
⊢ ∪ ran {⟨𝑣, 𝑢⟩} = 𝑢 |
48 | 46, 47 | eqtrdi 2226 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = ⟨𝑣, 𝑢⟩ → ∪
ran {𝑦} = 𝑢) |
49 | 48 | fveq2d 5519 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = ⟨𝑣, 𝑢⟩ → (𝑓‘∪ ran
{𝑦}) = (𝑓‘𝑢)) |
50 | 44, 49 | opeq12d 3786 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = ⟨𝑣, 𝑢⟩ → ⟨∪ dom {𝑦}, (𝑓‘∪ ran
{𝑦})⟩ = ⟨𝑣, (𝑓‘𝑢)⟩) |
51 | 37, 50 | eqeqan12d 2193 |
. . . . . . . . . . . . 13
⊢ ((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) → (⟨∪ dom {𝑥}, (𝑓‘∪ ran
{𝑥})⟩ = ⟨∪ dom {𝑦}, (𝑓‘∪ ran
{𝑦})⟩ ↔
⟨𝑧, (𝑓‘𝑤)⟩ = ⟨𝑣, (𝑓‘𝑢)⟩)) |
52 | 51 | ad2antlr 489 |
. . . . . . . . . . . 12
⊢
(((((𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐴) ∧ (𝑣 ∈ 𝐶 ∧ 𝑢 ∈ 𝐴)) ∧ (𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩)) ∧ 𝑓:𝐴–1-1→𝐵) → (⟨∪
dom {𝑥}, (𝑓‘∪ ran {𝑥})⟩ = ⟨∪
dom {𝑦}, (𝑓‘∪ ran {𝑦})⟩ ↔ ⟨𝑧, (𝑓‘𝑤)⟩ = ⟨𝑣, (𝑓‘𝑢)⟩)) |
53 | | eqeq12 2190 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) → (𝑥 = 𝑦 ↔ ⟨𝑧, 𝑤⟩ = ⟨𝑣, 𝑢⟩)) |
54 | 14, 16 | opth 4237 |
. . . . . . . . . . . . . 14
⊢
(⟨𝑧, 𝑤⟩ = ⟨𝑣, 𝑢⟩ ↔ (𝑧 = 𝑣 ∧ 𝑤 = 𝑢)) |
55 | 53, 54 | bitrdi 196 |
. . . . . . . . . . . . 13
⊢ ((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) → (𝑥 = 𝑦 ↔ (𝑧 = 𝑣 ∧ 𝑤 = 𝑢))) |
56 | 55 | ad2antlr 489 |
. . . . . . . . . . . 12
⊢
(((((𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐴) ∧ (𝑣 ∈ 𝐶 ∧ 𝑢 ∈ 𝐴)) ∧ (𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩)) ∧ 𝑓:𝐴–1-1→𝐵) → (𝑥 = 𝑦 ↔ (𝑧 = 𝑣 ∧ 𝑤 = 𝑢))) |
57 | 26, 52, 56 | 3bitr4d 220 |
. . . . . . . . . . 11
⊢
(((((𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐴) ∧ (𝑣 ∈ 𝐶 ∧ 𝑢 ∈ 𝐴)) ∧ (𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩)) ∧ 𝑓:𝐴–1-1→𝐵) → (⟨∪
dom {𝑥}, (𝑓‘∪ ran {𝑥})⟩ = ⟨∪
dom {𝑦}, (𝑓‘∪ ran {𝑦})⟩ ↔ 𝑥 = 𝑦)) |
58 | 57 | exp53 377 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐴) → ((𝑣 ∈ 𝐶 ∧ 𝑢 ∈ 𝐴) → (𝑥 = ⟨𝑧, 𝑤⟩ → (𝑦 = ⟨𝑣, 𝑢⟩ → (𝑓:𝐴–1-1→𝐵 → (⟨∪
dom {𝑥}, (𝑓‘∪ ran {𝑥})⟩ = ⟨∪
dom {𝑦}, (𝑓‘∪ ran {𝑦})⟩ ↔ 𝑥 = 𝑦)))))) |
59 | 58 | com23 78 |
. . . . . . . . 9
⊢ ((𝑧 ∈ 𝐶 ∧ 𝑤 ∈ 𝐴) → (𝑥 = ⟨𝑧, 𝑤⟩ → ((𝑣 ∈ 𝐶 ∧ 𝑢 ∈ 𝐴) → (𝑦 = ⟨𝑣, 𝑢⟩ → (𝑓:𝐴–1-1→𝐵 → (⟨∪
dom {𝑥}, (𝑓‘∪ ran {𝑥})⟩ = ⟨∪
dom {𝑦}, (𝑓‘∪ ran {𝑦})⟩ ↔ 𝑥 = 𝑦)))))) |
60 | 59 | rexlimivv 2600 |
. . . . . . . 8
⊢
(∃𝑧 ∈
𝐶 ∃𝑤 ∈ 𝐴 𝑥 = ⟨𝑧, 𝑤⟩ → ((𝑣 ∈ 𝐶 ∧ 𝑢 ∈ 𝐴) → (𝑦 = ⟨𝑣, 𝑢⟩ → (𝑓:𝐴–1-1→𝐵 → (⟨∪
dom {𝑥}, (𝑓‘∪ ran {𝑥})⟩ = ⟨∪
dom {𝑦}, (𝑓‘∪ ran {𝑦})⟩ ↔ 𝑥 = 𝑦))))) |
61 | 60 | rexlimdvv 2601 |
. . . . . . 7
⊢
(∃𝑧 ∈
𝐶 ∃𝑤 ∈ 𝐴 𝑥 = ⟨𝑧, 𝑤⟩ → (∃𝑣 ∈ 𝐶 ∃𝑢 ∈ 𝐴 𝑦 = ⟨𝑣, 𝑢⟩ → (𝑓:𝐴–1-1→𝐵 → (⟨∪
dom {𝑥}, (𝑓‘∪ ran {𝑥})⟩ = ⟨∪
dom {𝑦}, (𝑓‘∪ ran {𝑦})⟩ ↔ 𝑥 = 𝑦)))) |
62 | 61 | imp 124 |
. . . . . 6
⊢
((∃𝑧 ∈
𝐶 ∃𝑤 ∈ 𝐴 𝑥 = ⟨𝑧, 𝑤⟩ ∧ ∃𝑣 ∈ 𝐶 ∃𝑢 ∈ 𝐴 𝑦 = ⟨𝑣, 𝑢⟩) → (𝑓:𝐴–1-1→𝐵 → (⟨∪
dom {𝑥}, (𝑓‘∪ ran {𝑥})⟩ = ⟨∪
dom {𝑦}, (𝑓‘∪ ran {𝑦})⟩ ↔ 𝑥 = 𝑦))) |
63 | 12, 13, 62 | syl2anb 291 |
. . . . 5
⊢ ((𝑥 ∈ (𝐶 × 𝐴) ∧ 𝑦 ∈ (𝐶 × 𝐴)) → (𝑓:𝐴–1-1→𝐵 → (⟨∪
dom {𝑥}, (𝑓‘∪ ran {𝑥})⟩ = ⟨∪
dom {𝑦}, (𝑓‘∪ ran {𝑦})⟩ ↔ 𝑥 = 𝑦))) |
64 | 63 | com12 30 |
. . . 4
⊢ (𝑓:𝐴–1-1→𝐵 → ((𝑥 ∈ (𝐶 × 𝐴) ∧ 𝑦 ∈ (𝐶 × 𝐴)) → (⟨∪ dom {𝑥}, (𝑓‘∪ ran
{𝑥})⟩ = ⟨∪ dom {𝑦}, (𝑓‘∪ ran
{𝑦})⟩ ↔ 𝑥 = 𝑦))) |
65 | 64 | adantl 277 |
. . 3
⊢ ((𝐴 ≼ 𝐵 ∧ 𝑓:𝐴–1-1→𝐵) → ((𝑥 ∈ (𝐶 × 𝐴) ∧ 𝑦 ∈ (𝐶 × 𝐴)) → (⟨∪ dom {𝑥}, (𝑓‘∪ ran
{𝑥})⟩ = ⟨∪ dom {𝑦}, (𝑓‘∪ ran
{𝑦})⟩ ↔ 𝑥 = 𝑦))) |
66 | | xpdom.2 |
. . . . 5
⊢ 𝐶 ∈ V |
67 | | reldom 6744 |
. . . . . 6
⊢ Rel
≼ |
68 | 67 | brrelex1i 4669 |
. . . . 5
⊢ (𝐴 ≼ 𝐵 → 𝐴 ∈ V) |
69 | | xpexg 4740 |
. . . . 5
⊢ ((𝐶 ∈ V ∧ 𝐴 ∈ V) → (𝐶 × 𝐴) ∈ V) |
70 | 66, 68, 69 | sylancr 414 |
. . . 4
⊢ (𝐴 ≼ 𝐵 → (𝐶 × 𝐴) ∈ V) |
71 | 70 | adantr 276 |
. . 3
⊢ ((𝐴 ≼ 𝐵 ∧ 𝑓:𝐴–1-1→𝐵) → (𝐶 × 𝐴) ∈ V) |
72 | 67 | brrelex2i 4670 |
. . . . 5
⊢ (𝐴 ≼ 𝐵 → 𝐵 ∈ V) |
73 | | xpexg 4740 |
. . . . 5
⊢ ((𝐶 ∈ V ∧ 𝐵 ∈ V) → (𝐶 × 𝐵) ∈ V) |
74 | 66, 72, 73 | sylancr 414 |
. . . 4
⊢ (𝐴 ≼ 𝐵 → (𝐶 × 𝐵) ∈ V) |
75 | 74 | adantr 276 |
. . 3
⊢ ((𝐴 ≼ 𝐵 ∧ 𝑓:𝐴–1-1→𝐵) → (𝐶 × 𝐵) ∈ V) |
76 | 11, 65, 71, 75 | dom3d 6773 |
. 2
⊢ ((𝐴 ≼ 𝐵 ∧ 𝑓:𝐴–1-1→𝐵) → (𝐶 × 𝐴) ≼ (𝐶 × 𝐵)) |
77 | 1, 76 | exlimddv 1898 |
1
⊢ (𝐴 ≼ 𝐵 → (𝐶 × 𝐴) ≼ (𝐶 × 𝐵)) |