Step | Hyp | Ref
| Expression |
1 | | ensym 8271 |
. 2
⊢ ((𝐴 × 𝐴) ≈ (𝐵 ∪ 𝐶) → (𝐵 ∪ 𝐶) ≈ (𝐴 × 𝐴)) |
2 | | bren 8231 |
. . 3
⊢ ((𝐵 ∪ 𝐶) ≈ (𝐴 × 𝐴) ↔ ∃𝑓 𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴)) |
3 | | ssdif0 4171 |
. . . . . 6
⊢ (𝐴 ⊆ (((1st
↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵) ↔ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) = ∅) |
4 | | dmxpid 5577 |
. . . . . . . . . . . . . 14
⊢ dom
(𝐴 × 𝐴) = 𝐴 |
5 | | f1ofo 6385 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) → 𝑓:(𝐵 ∪ 𝐶)–onto→(𝐴 × 𝐴)) |
6 | | forn 6356 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓:(𝐵 ∪ 𝐶)–onto→(𝐴 × 𝐴) → ran 𝑓 = (𝐴 × 𝐴)) |
7 | 5, 6 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) → ran 𝑓 = (𝐴 × 𝐴)) |
8 | | vex 3417 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑓 ∈ V |
9 | 8 | rnex 7362 |
. . . . . . . . . . . . . . . 16
⊢ ran 𝑓 ∈ V |
10 | 7, 9 | syl6eqelr 2915 |
. . . . . . . . . . . . . . 15
⊢ (𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) → (𝐴 × 𝐴) ∈ V) |
11 | 10 | dmexd 7360 |
. . . . . . . . . . . . . 14
⊢ (𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) → dom (𝐴 × 𝐴) ∈ V) |
12 | 4, 11 | syl5eqelr 2911 |
. . . . . . . . . . . . 13
⊢ (𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) → 𝐴 ∈ V) |
13 | | imassrn 5718 |
. . . . . . . . . . . . . 14
⊢
(((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵) ⊆ ran ((1st ↾
(𝐴 × 𝐴)) ∘ 𝑓) |
14 | | f1stres 7452 |
. . . . . . . . . . . . . . . 16
⊢
(1st ↾ (𝐴 × 𝐴)):(𝐴 × 𝐴)⟶𝐴 |
15 | | f1of 6378 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) → 𝑓:(𝐵 ∪ 𝐶)⟶(𝐴 × 𝐴)) |
16 | | fco 6295 |
. . . . . . . . . . . . . . . 16
⊢
(((1st ↾ (𝐴 × 𝐴)):(𝐴 × 𝐴)⟶𝐴 ∧ 𝑓:(𝐵 ∪ 𝐶)⟶(𝐴 × 𝐴)) → ((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓):(𝐵 ∪ 𝐶)⟶𝐴) |
17 | 14, 15, 16 | sylancr 583 |
. . . . . . . . . . . . . . 15
⊢ (𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) → ((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓):(𝐵 ∪ 𝐶)⟶𝐴) |
18 | 17 | frnd 6285 |
. . . . . . . . . . . . . 14
⊢ (𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) → ran ((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) ⊆ 𝐴) |
19 | 13, 18 | syl5ss 3838 |
. . . . . . . . . . . . 13
⊢ (𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) → (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵) ⊆ 𝐴) |
20 | 12, 19 | ssexd 5030 |
. . . . . . . . . . . 12
⊢ (𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) → (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵) ∈ V) |
21 | 20 | adantr 474 |
. . . . . . . . . . 11
⊢ ((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝐴 ⊆ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) → (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵) ∈ V) |
22 | | simpr 479 |
. . . . . . . . . . 11
⊢ ((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝐴 ⊆ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) → 𝐴 ⊆ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) |
23 | | ssdomg 8268 |
. . . . . . . . . . 11
⊢
((((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵) ∈ V → (𝐴 ⊆ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵) → 𝐴 ≼ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) |
24 | 21, 22, 23 | sylc 65 |
. . . . . . . . . 10
⊢ ((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝐴 ⊆ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) → 𝐴 ≼ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) |
25 | | domwdom 8748 |
. . . . . . . . . 10
⊢ (𝐴 ≼ (((1st
↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵) → 𝐴 ≼* (((1st
↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) |
26 | 24, 25 | syl 17 |
. . . . . . . . 9
⊢ ((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝐴 ⊆ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) → 𝐴 ≼* (((1st
↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) |
27 | 17 | ffund 6282 |
. . . . . . . . . . 11
⊢ (𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) → Fun ((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓)) |
28 | | ssun1 4003 |
. . . . . . . . . . . 12
⊢ 𝐵 ⊆ (𝐵 ∪ 𝐶) |
29 | | f1odm 6382 |
. . . . . . . . . . . . 13
⊢ (𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) → dom 𝑓 = (𝐵 ∪ 𝐶)) |
30 | 8 | dmex 7361 |
. . . . . . . . . . . . 13
⊢ dom 𝑓 ∈ V |
31 | 29, 30 | syl6eqelr 2915 |
. . . . . . . . . . . 12
⊢ (𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) → (𝐵 ∪ 𝐶) ∈ V) |
32 | | ssexg 5029 |
. . . . . . . . . . . 12
⊢ ((𝐵 ⊆ (𝐵 ∪ 𝐶) ∧ (𝐵 ∪ 𝐶) ∈ V) → 𝐵 ∈ V) |
33 | 28, 31, 32 | sylancr 583 |
. . . . . . . . . . 11
⊢ (𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) → 𝐵 ∈ V) |
34 | | wdomima2g 8760 |
. . . . . . . . . . 11
⊢ ((Fun
((1st ↾ (𝐴
× 𝐴)) ∘ 𝑓) ∧ 𝐵 ∈ V ∧ (((1st ↾
(𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵) ∈ V) → (((1st ↾
(𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵) ≼* 𝐵) |
35 | 27, 33, 20, 34 | syl3anc 1496 |
. . . . . . . . . 10
⊢ (𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) → (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵) ≼* 𝐵) |
36 | 35 | adantr 474 |
. . . . . . . . 9
⊢ ((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝐴 ⊆ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) → (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵) ≼* 𝐵) |
37 | | wdomtr 8749 |
. . . . . . . . 9
⊢ ((𝐴 ≼*
(((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵) ∧ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵) ≼* 𝐵) → 𝐴 ≼* 𝐵) |
38 | 26, 36, 37 | syl2anc 581 |
. . . . . . . 8
⊢ ((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝐴 ⊆ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) → 𝐴 ≼* 𝐵) |
39 | 38 | orcd 906 |
. . . . . . 7
⊢ ((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝐴 ⊆ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) → (𝐴 ≼* 𝐵 ∨ 𝐴 ≼ 𝐶)) |
40 | 39 | ex 403 |
. . . . . 6
⊢ (𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) → (𝐴 ⊆ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵) → (𝐴 ≼* 𝐵 ∨ 𝐴 ≼ 𝐶))) |
41 | 3, 40 | syl5bir 235 |
. . . . 5
⊢ (𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) → ((𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) = ∅ → (𝐴 ≼* 𝐵 ∨ 𝐴 ≼ 𝐶))) |
42 | | n0 4160 |
. . . . . 6
⊢ ((𝐴 ∖ (((1st
↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) ≠ ∅ ↔ ∃𝑥 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) |
43 | | ssun2 4004 |
. . . . . . . . . . . . 13
⊢ 𝐶 ⊆ (𝐵 ∪ 𝐶) |
44 | | ssexg 5029 |
. . . . . . . . . . . . 13
⊢ ((𝐶 ⊆ (𝐵 ∪ 𝐶) ∧ (𝐵 ∪ 𝐶) ∈ V) → 𝐶 ∈ V) |
45 | 43, 31, 44 | sylancr 583 |
. . . . . . . . . . . 12
⊢ (𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) → 𝐶 ∈ V) |
46 | 45 | adantr 474 |
. . . . . . . . . . 11
⊢ ((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → 𝐶 ∈ V) |
47 | | f1ofn 6379 |
. . . . . . . . . . . . . . 15
⊢ (𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) → 𝑓 Fn (𝐵 ∪ 𝐶)) |
48 | | elpreima 6586 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 Fn (𝐵 ∪ 𝐶) → (𝑦 ∈ (◡𝑓 “ ({𝑥} × 𝐴)) ↔ (𝑦 ∈ (𝐵 ∪ 𝐶) ∧ (𝑓‘𝑦) ∈ ({𝑥} × 𝐴)))) |
49 | 47, 48 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) → (𝑦 ∈ (◡𝑓 “ ({𝑥} × 𝐴)) ↔ (𝑦 ∈ (𝐵 ∪ 𝐶) ∧ (𝑓‘𝑦) ∈ ({𝑥} × 𝐴)))) |
50 | 49 | adantr 474 |
. . . . . . . . . . . . 13
⊢ ((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → (𝑦 ∈ (◡𝑓 “ ({𝑥} × 𝐴)) ↔ (𝑦 ∈ (𝐵 ∪ 𝐶) ∧ (𝑓‘𝑦) ∈ ({𝑥} × 𝐴)))) |
51 | | elun 3980 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ (𝐵 ∪ 𝐶) ↔ (𝑦 ∈ 𝐵 ∨ 𝑦 ∈ 𝐶)) |
52 | | df-or 881 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ 𝐵 ∨ 𝑦 ∈ 𝐶) ↔ (¬ 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶)) |
53 | 51, 52 | bitri 267 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ (𝐵 ∪ 𝐶) ↔ (¬ 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶)) |
54 | | eldifn 3960 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) → ¬ 𝑥 ∈ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) |
55 | 54 | ad2antlr 720 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ (𝑓‘𝑦) ∈ ({𝑥} × 𝐴)) → ¬ 𝑥 ∈ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) |
56 | 15 | ad2antrr 719 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓‘𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦 ∈ 𝐵)) → 𝑓:(𝐵 ∪ 𝐶)⟶(𝐴 × 𝐴)) |
57 | | simprr 791 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓‘𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦 ∈ 𝐵)) → 𝑦 ∈ 𝐵) |
58 | 28, 57 | sseldi 3825 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓‘𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦 ∈ 𝐵)) → 𝑦 ∈ (𝐵 ∪ 𝐶)) |
59 | | fvco3 6522 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑓:(𝐵 ∪ 𝐶)⟶(𝐴 × 𝐴) ∧ 𝑦 ∈ (𝐵 ∪ 𝐶)) → (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓)‘𝑦) = ((1st ↾ (𝐴 × 𝐴))‘(𝑓‘𝑦))) |
60 | 56, 58, 59 | syl2anc 581 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓‘𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦 ∈ 𝐵)) → (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓)‘𝑦) = ((1st ↾ (𝐴 × 𝐴))‘(𝑓‘𝑦))) |
61 | | eldifi 3959 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) → 𝑥 ∈ 𝐴) |
62 | 61 | adantl 475 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → 𝑥 ∈ 𝐴) |
63 | 62 | snssd 4558 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → {𝑥} ⊆ 𝐴) |
64 | | xpss1 5361 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ({𝑥} ⊆ 𝐴 → ({𝑥} × 𝐴) ⊆ (𝐴 × 𝐴)) |
65 | 63, 64 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → ({𝑥} × 𝐴) ⊆ (𝐴 × 𝐴)) |
66 | 65 | adantr 474 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓‘𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦 ∈ 𝐵)) → ({𝑥} × 𝐴) ⊆ (𝐴 × 𝐴)) |
67 | | simprl 789 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓‘𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦 ∈ 𝐵)) → (𝑓‘𝑦) ∈ ({𝑥} × 𝐴)) |
68 | 66, 67 | sseldd 3828 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓‘𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦 ∈ 𝐵)) → (𝑓‘𝑦) ∈ (𝐴 × 𝐴)) |
69 | | fvres 6452 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑓‘𝑦) ∈ (𝐴 × 𝐴) → ((1st ↾ (𝐴 × 𝐴))‘(𝑓‘𝑦)) = (1st ‘(𝑓‘𝑦))) |
70 | 68, 69 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓‘𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦 ∈ 𝐵)) → ((1st ↾ (𝐴 × 𝐴))‘(𝑓‘𝑦)) = (1st ‘(𝑓‘𝑦))) |
71 | | xp1st 7460 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑓‘𝑦) ∈ ({𝑥} × 𝐴) → (1st ‘(𝑓‘𝑦)) ∈ {𝑥}) |
72 | 67, 71 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓‘𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦 ∈ 𝐵)) → (1st ‘(𝑓‘𝑦)) ∈ {𝑥}) |
73 | 70, 72 | eqeltrd 2906 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓‘𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦 ∈ 𝐵)) → ((1st ↾ (𝐴 × 𝐴))‘(𝑓‘𝑦)) ∈ {𝑥}) |
74 | | elsni 4414 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((1st ↾ (𝐴 × 𝐴))‘(𝑓‘𝑦)) ∈ {𝑥} → ((1st ↾ (𝐴 × 𝐴))‘(𝑓‘𝑦)) = 𝑥) |
75 | 73, 74 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓‘𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦 ∈ 𝐵)) → ((1st ↾ (𝐴 × 𝐴))‘(𝑓‘𝑦)) = 𝑥) |
76 | 60, 75 | eqtrd 2861 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓‘𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦 ∈ 𝐵)) → (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓)‘𝑦) = 𝑥) |
77 | 17 | ffnd 6279 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) → ((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) Fn (𝐵 ∪ 𝐶)) |
78 | 77 | ad2antrr 719 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓‘𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦 ∈ 𝐵)) → ((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) Fn (𝐵 ∪ 𝐶)) |
79 | 28 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓‘𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦 ∈ 𝐵)) → 𝐵 ⊆ (𝐵 ∪ 𝐶)) |
80 | | fnfvima 6752 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) Fn (𝐵 ∪ 𝐶) ∧ 𝐵 ⊆ (𝐵 ∪ 𝐶) ∧ 𝑦 ∈ 𝐵) → (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓)‘𝑦) ∈ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) |
81 | 78, 79, 57, 80 | syl3anc 1496 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓‘𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦 ∈ 𝐵)) → (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓)‘𝑦) ∈ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) |
82 | 76, 81 | eqeltrrd 2907 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ ((𝑓‘𝑦) ∈ ({𝑥} × 𝐴) ∧ 𝑦 ∈ 𝐵)) → 𝑥 ∈ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) |
83 | 82 | expr 450 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ (𝑓‘𝑦) ∈ ({𝑥} × 𝐴)) → (𝑦 ∈ 𝐵 → 𝑥 ∈ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) |
84 | 55, 83 | mtod 190 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) ∧ (𝑓‘𝑦) ∈ ({𝑥} × 𝐴)) → ¬ 𝑦 ∈ 𝐵) |
85 | 84 | ex 403 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → ((𝑓‘𝑦) ∈ ({𝑥} × 𝐴) → ¬ 𝑦 ∈ 𝐵)) |
86 | 85 | imim1d 82 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → ((¬ 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) → ((𝑓‘𝑦) ∈ ({𝑥} × 𝐴) → 𝑦 ∈ 𝐶))) |
87 | 53, 86 | syl5bi 234 |
. . . . . . . . . . . . . 14
⊢ ((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → (𝑦 ∈ (𝐵 ∪ 𝐶) → ((𝑓‘𝑦) ∈ ({𝑥} × 𝐴) → 𝑦 ∈ 𝐶))) |
88 | 87 | impd 400 |
. . . . . . . . . . . . 13
⊢ ((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → ((𝑦 ∈ (𝐵 ∪ 𝐶) ∧ (𝑓‘𝑦) ∈ ({𝑥} × 𝐴)) → 𝑦 ∈ 𝐶)) |
89 | 50, 88 | sylbid 232 |
. . . . . . . . . . . 12
⊢ ((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → (𝑦 ∈ (◡𝑓 “ ({𝑥} × 𝐴)) → 𝑦 ∈ 𝐶)) |
90 | 89 | ssrdv 3833 |
. . . . . . . . . . 11
⊢ ((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → (◡𝑓 “ ({𝑥} × 𝐴)) ⊆ 𝐶) |
91 | | ssdomg 8268 |
. . . . . . . . . . 11
⊢ (𝐶 ∈ V → ((◡𝑓 “ ({𝑥} × 𝐴)) ⊆ 𝐶 → (◡𝑓 “ ({𝑥} × 𝐴)) ≼ 𝐶)) |
92 | 46, 90, 91 | sylc 65 |
. . . . . . . . . 10
⊢ ((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → (◡𝑓 “ ({𝑥} × 𝐴)) ≼ 𝐶) |
93 | | f1ocnv 6390 |
. . . . . . . . . . . . . . 15
⊢ (𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) → ◡𝑓:(𝐴 × 𝐴)–1-1-onto→(𝐵 ∪ 𝐶)) |
94 | | f1of1 6377 |
. . . . . . . . . . . . . . 15
⊢ (◡𝑓:(𝐴 × 𝐴)–1-1-onto→(𝐵 ∪ 𝐶) → ◡𝑓:(𝐴 × 𝐴)–1-1→(𝐵 ∪ 𝐶)) |
95 | 93, 94 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) → ◡𝑓:(𝐴 × 𝐴)–1-1→(𝐵 ∪ 𝐶)) |
96 | 95 | adantr 474 |
. . . . . . . . . . . . 13
⊢ ((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → ◡𝑓:(𝐴 × 𝐴)–1-1→(𝐵 ∪ 𝐶)) |
97 | 31 | adantr 474 |
. . . . . . . . . . . . 13
⊢ ((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → (𝐵 ∪ 𝐶) ∈ V) |
98 | | snex 5129 |
. . . . . . . . . . . . . 14
⊢ {𝑥} ∈ V |
99 | 12 | adantr 474 |
. . . . . . . . . . . . . 14
⊢ ((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → 𝐴 ∈ V) |
100 | | xpexg 7220 |
. . . . . . . . . . . . . 14
⊢ (({𝑥} ∈ V ∧ 𝐴 ∈ V) → ({𝑥} × 𝐴) ∈ V) |
101 | 98, 99, 100 | sylancr 583 |
. . . . . . . . . . . . 13
⊢ ((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → ({𝑥} × 𝐴) ∈ V) |
102 | | f1imaen2g 8283 |
. . . . . . . . . . . . 13
⊢ (((◡𝑓:(𝐴 × 𝐴)–1-1→(𝐵 ∪ 𝐶) ∧ (𝐵 ∪ 𝐶) ∈ V) ∧ (({𝑥} × 𝐴) ⊆ (𝐴 × 𝐴) ∧ ({𝑥} × 𝐴) ∈ V)) → (◡𝑓 “ ({𝑥} × 𝐴)) ≈ ({𝑥} × 𝐴)) |
103 | 96, 97, 65, 101, 102 | syl22anc 874 |
. . . . . . . . . . . 12
⊢ ((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → (◡𝑓 “ ({𝑥} × 𝐴)) ≈ ({𝑥} × 𝐴)) |
104 | | vex 3417 |
. . . . . . . . . . . . 13
⊢ 𝑥 ∈ V |
105 | | xpsnen2g 8322 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ V ∧ 𝐴 ∈ V) → ({𝑥} × 𝐴) ≈ 𝐴) |
106 | 104, 99, 105 | sylancr 583 |
. . . . . . . . . . . 12
⊢ ((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → ({𝑥} × 𝐴) ≈ 𝐴) |
107 | | entr 8274 |
. . . . . . . . . . . 12
⊢ (((◡𝑓 “ ({𝑥} × 𝐴)) ≈ ({𝑥} × 𝐴) ∧ ({𝑥} × 𝐴) ≈ 𝐴) → (◡𝑓 “ ({𝑥} × 𝐴)) ≈ 𝐴) |
108 | 103, 106,
107 | syl2anc 581 |
. . . . . . . . . . 11
⊢ ((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → (◡𝑓 “ ({𝑥} × 𝐴)) ≈ 𝐴) |
109 | | domen1 8371 |
. . . . . . . . . . 11
⊢ ((◡𝑓 “ ({𝑥} × 𝐴)) ≈ 𝐴 → ((◡𝑓 “ ({𝑥} × 𝐴)) ≼ 𝐶 ↔ 𝐴 ≼ 𝐶)) |
110 | 108, 109 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → ((◡𝑓 “ ({𝑥} × 𝐴)) ≼ 𝐶 ↔ 𝐴 ≼ 𝐶)) |
111 | 92, 110 | mpbid 224 |
. . . . . . . . 9
⊢ ((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → 𝐴 ≼ 𝐶) |
112 | 111 | olcd 907 |
. . . . . . . 8
⊢ ((𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) ∧ 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵))) → (𝐴 ≼* 𝐵 ∨ 𝐴 ≼ 𝐶)) |
113 | 112 | ex 403 |
. . . . . . 7
⊢ (𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) → (𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) → (𝐴 ≼* 𝐵 ∨ 𝐴 ≼ 𝐶))) |
114 | 113 | exlimdv 2034 |
. . . . . 6
⊢ (𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) → (∃𝑥 𝑥 ∈ (𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) → (𝐴 ≼* 𝐵 ∨ 𝐴 ≼ 𝐶))) |
115 | 42, 114 | syl5bi 234 |
. . . . 5
⊢ (𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) → ((𝐴 ∖ (((1st ↾ (𝐴 × 𝐴)) ∘ 𝑓) “ 𝐵)) ≠ ∅ → (𝐴 ≼* 𝐵 ∨ 𝐴 ≼ 𝐶))) |
116 | 41, 115 | pm2.61dne 3085 |
. . . 4
⊢ (𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) → (𝐴 ≼* 𝐵 ∨ 𝐴 ≼ 𝐶)) |
117 | 116 | exlimiv 2031 |
. . 3
⊢
(∃𝑓 𝑓:(𝐵 ∪ 𝐶)–1-1-onto→(𝐴 × 𝐴) → (𝐴 ≼* 𝐵 ∨ 𝐴 ≼ 𝐶)) |
118 | 2, 117 | sylbi 209 |
. 2
⊢ ((𝐵 ∪ 𝐶) ≈ (𝐴 × 𝐴) → (𝐴 ≼* 𝐵 ∨ 𝐴 ≼ 𝐶)) |
119 | 1, 118 | syl 17 |
1
⊢ ((𝐴 × 𝐴) ≈ (𝐵 ∪ 𝐶) → (𝐴 ≼* 𝐵 ∨ 𝐴 ≼ 𝐶)) |