Step | Hyp | Ref
| Expression |
1 | | vex 3176 |
. . 3
⊢ 𝑎 ∈ V |
2 | | 1sdom 8048 |
. . 3
⊢ (𝑎 ∈ V →
(1𝑜 ≺ 𝑎 ↔ ∃𝑚 ∈ 𝑎 ∃𝑛 ∈ 𝑎 ¬ 𝑚 = 𝑛)) |
3 | 1, 2 | ax-mp 5 |
. 2
⊢
(1𝑜 ≺ 𝑎 ↔ ∃𝑚 ∈ 𝑎 ∃𝑛 ∈ 𝑎 ¬ 𝑚 = 𝑛) |
4 | | vex 3176 |
. . 3
⊢ 𝑏 ∈ V |
5 | | 1sdom 8048 |
. . 3
⊢ (𝑏 ∈ V →
(1𝑜 ≺ 𝑏 ↔ ∃𝑠 ∈ 𝑏 ∃𝑡 ∈ 𝑏 ¬ 𝑠 = 𝑡)) |
6 | 4, 5 | ax-mp 5 |
. 2
⊢
(1𝑜 ≺ 𝑏 ↔ ∃𝑠 ∈ 𝑏 ∃𝑡 ∈ 𝑏 ¬ 𝑠 = 𝑡) |
7 | | reeanv 3086 |
. . 3
⊢
(∃𝑚 ∈
𝑎 ∃𝑠 ∈ 𝑏 (∃𝑛 ∈ 𝑎 ¬ 𝑚 = 𝑛 ∧ ∃𝑡 ∈ 𝑏 ¬ 𝑠 = 𝑡) ↔ (∃𝑚 ∈ 𝑎 ∃𝑛 ∈ 𝑎 ¬ 𝑚 = 𝑛 ∧ ∃𝑠 ∈ 𝑏 ∃𝑡 ∈ 𝑏 ¬ 𝑠 = 𝑡)) |
8 | | reeanv 3086 |
. . . . 5
⊢
(∃𝑛 ∈
𝑎 ∃𝑡 ∈ 𝑏 (¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡) ↔ (∃𝑛 ∈ 𝑎 ¬ 𝑚 = 𝑛 ∧ ∃𝑡 ∈ 𝑏 ¬ 𝑠 = 𝑡)) |
9 | | unxpdomlem1.2 |
. . . . . . . . . . 11
⊢ 𝐺 = if(𝑥 ∈ 𝑎, 〈𝑥, if(𝑥 = 𝑚, 𝑡, 𝑠)〉, 〈if(𝑥 = 𝑡, 𝑛, 𝑚), 𝑥〉) |
10 | | simpr 476 |
. . . . . . . . . . . . 13
⊢
(((((𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏) ∧ (𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏) ∧ (¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡)) ∧ 𝑥 ∈ (𝑎 ∪ 𝑏)) ∧ 𝑥 ∈ 𝑎) → 𝑥 ∈ 𝑎) |
11 | | simp2r 1081 |
. . . . . . . . . . . . . . 15
⊢ (((𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏) ∧ (𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏) ∧ (¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡)) → 𝑡 ∈ 𝑏) |
12 | | simp1r 1079 |
. . . . . . . . . . . . . . 15
⊢ (((𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏) ∧ (𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏) ∧ (¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡)) → 𝑠 ∈ 𝑏) |
13 | 11, 12 | ifcld 4081 |
. . . . . . . . . . . . . 14
⊢ (((𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏) ∧ (𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏) ∧ (¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡)) → if(𝑥 = 𝑚, 𝑡, 𝑠) ∈ 𝑏) |
14 | 13 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢
(((((𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏) ∧ (𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏) ∧ (¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡)) ∧ 𝑥 ∈ (𝑎 ∪ 𝑏)) ∧ 𝑥 ∈ 𝑎) → if(𝑥 = 𝑚, 𝑡, 𝑠) ∈ 𝑏) |
15 | | opelxpi 5072 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝑎 ∧ if(𝑥 = 𝑚, 𝑡, 𝑠) ∈ 𝑏) → 〈𝑥, if(𝑥 = 𝑚, 𝑡, 𝑠)〉 ∈ (𝑎 × 𝑏)) |
16 | 10, 14, 15 | syl2anc 691 |
. . . . . . . . . . . 12
⊢
(((((𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏) ∧ (𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏) ∧ (¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡)) ∧ 𝑥 ∈ (𝑎 ∪ 𝑏)) ∧ 𝑥 ∈ 𝑎) → 〈𝑥, if(𝑥 = 𝑚, 𝑡, 𝑠)〉 ∈ (𝑎 × 𝑏)) |
17 | | simp2l 1080 |
. . . . . . . . . . . . . . 15
⊢ (((𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏) ∧ (𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏) ∧ (¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡)) → 𝑛 ∈ 𝑎) |
18 | | simp1l 1078 |
. . . . . . . . . . . . . . 15
⊢ (((𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏) ∧ (𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏) ∧ (¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡)) → 𝑚 ∈ 𝑎) |
19 | 17, 18 | ifcld 4081 |
. . . . . . . . . . . . . 14
⊢ (((𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏) ∧ (𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏) ∧ (¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡)) → if(𝑥 = 𝑡, 𝑛, 𝑚) ∈ 𝑎) |
20 | 19 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢
(((((𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏) ∧ (𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏) ∧ (¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡)) ∧ 𝑥 ∈ (𝑎 ∪ 𝑏)) ∧ ¬ 𝑥 ∈ 𝑎) → if(𝑥 = 𝑡, 𝑛, 𝑚) ∈ 𝑎) |
21 | | simpr 476 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏) ∧ (𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏) ∧ (¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡)) ∧ 𝑥 ∈ (𝑎 ∪ 𝑏)) → 𝑥 ∈ (𝑎 ∪ 𝑏)) |
22 | | elun 3715 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (𝑎 ∪ 𝑏) ↔ (𝑥 ∈ 𝑎 ∨ 𝑥 ∈ 𝑏)) |
23 | 21, 22 | sylib 207 |
. . . . . . . . . . . . . 14
⊢ ((((𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏) ∧ (𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏) ∧ (¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡)) ∧ 𝑥 ∈ (𝑎 ∪ 𝑏)) → (𝑥 ∈ 𝑎 ∨ 𝑥 ∈ 𝑏)) |
24 | 23 | orcanai 950 |
. . . . . . . . . . . . 13
⊢
(((((𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏) ∧ (𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏) ∧ (¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡)) ∧ 𝑥 ∈ (𝑎 ∪ 𝑏)) ∧ ¬ 𝑥 ∈ 𝑎) → 𝑥 ∈ 𝑏) |
25 | | opelxpi 5072 |
. . . . . . . . . . . . 13
⊢
((if(𝑥 = 𝑡, 𝑛, 𝑚) ∈ 𝑎 ∧ 𝑥 ∈ 𝑏) → 〈if(𝑥 = 𝑡, 𝑛, 𝑚), 𝑥〉 ∈ (𝑎 × 𝑏)) |
26 | 20, 24, 25 | syl2anc 691 |
. . . . . . . . . . . 12
⊢
(((((𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏) ∧ (𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏) ∧ (¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡)) ∧ 𝑥 ∈ (𝑎 ∪ 𝑏)) ∧ ¬ 𝑥 ∈ 𝑎) → 〈if(𝑥 = 𝑡, 𝑛, 𝑚), 𝑥〉 ∈ (𝑎 × 𝑏)) |
27 | 16, 26 | ifclda 4070 |
. . . . . . . . . . 11
⊢ ((((𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏) ∧ (𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏) ∧ (¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡)) ∧ 𝑥 ∈ (𝑎 ∪ 𝑏)) → if(𝑥 ∈ 𝑎, 〈𝑥, if(𝑥 = 𝑚, 𝑡, 𝑠)〉, 〈if(𝑥 = 𝑡, 𝑛, 𝑚), 𝑥〉) ∈ (𝑎 × 𝑏)) |
28 | 9, 27 | syl5eqel 2692 |
. . . . . . . . . 10
⊢ ((((𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏) ∧ (𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏) ∧ (¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡)) ∧ 𝑥 ∈ (𝑎 ∪ 𝑏)) → 𝐺 ∈ (𝑎 × 𝑏)) |
29 | | unxpdomlem1.1 |
. . . . . . . . . 10
⊢ 𝐹 = (𝑥 ∈ (𝑎 ∪ 𝑏) ↦ 𝐺) |
30 | 28, 29 | fmptd 6292 |
. . . . . . . . 9
⊢ (((𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏) ∧ (𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏) ∧ (¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡)) → 𝐹:(𝑎 ∪ 𝑏)⟶(𝑎 × 𝑏)) |
31 | 29, 9 | unxpdomlem1 8049 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ (𝑎 ∪ 𝑏) → (𝐹‘𝑧) = if(𝑧 ∈ 𝑎, 〈𝑧, if(𝑧 = 𝑚, 𝑡, 𝑠)〉, 〈if(𝑧 = 𝑡, 𝑛, 𝑚), 𝑧〉)) |
32 | 31 | ad2antrl 760 |
. . . . . . . . . . . . . . 15
⊢ (((¬
𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡) ∧ (𝑧 ∈ (𝑎 ∪ 𝑏) ∧ 𝑤 ∈ (𝑎 ∪ 𝑏))) → (𝐹‘𝑧) = if(𝑧 ∈ 𝑎, 〈𝑧, if(𝑧 = 𝑚, 𝑡, 𝑠)〉, 〈if(𝑧 = 𝑡, 𝑛, 𝑚), 𝑧〉)) |
33 | | iftrue 4042 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ 𝑎 → if(𝑧 ∈ 𝑎, 〈𝑧, if(𝑧 = 𝑚, 𝑡, 𝑠)〉, 〈if(𝑧 = 𝑡, 𝑛, 𝑚), 𝑧〉) = 〈𝑧, if(𝑧 = 𝑚, 𝑡, 𝑠)〉) |
34 | 33 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝑧 ∈ 𝑎 ∧ 𝑤 ∈ 𝑎) → if(𝑧 ∈ 𝑎, 〈𝑧, if(𝑧 = 𝑚, 𝑡, 𝑠)〉, 〈if(𝑧 = 𝑡, 𝑛, 𝑚), 𝑧〉) = 〈𝑧, if(𝑧 = 𝑚, 𝑡, 𝑠)〉) |
35 | 32, 34 | sylan9eq 2664 |
. . . . . . . . . . . . . 14
⊢ ((((¬
𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡) ∧ (𝑧 ∈ (𝑎 ∪ 𝑏) ∧ 𝑤 ∈ (𝑎 ∪ 𝑏))) ∧ (𝑧 ∈ 𝑎 ∧ 𝑤 ∈ 𝑎)) → (𝐹‘𝑧) = 〈𝑧, if(𝑧 = 𝑚, 𝑡, 𝑠)〉) |
36 | 29, 9 | unxpdomlem1 8049 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 ∈ (𝑎 ∪ 𝑏) → (𝐹‘𝑤) = if(𝑤 ∈ 𝑎, 〈𝑤, if(𝑤 = 𝑚, 𝑡, 𝑠)〉, 〈if(𝑤 = 𝑡, 𝑛, 𝑚), 𝑤〉)) |
37 | 36 | ad2antll 761 |
. . . . . . . . . . . . . . 15
⊢ (((¬
𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡) ∧ (𝑧 ∈ (𝑎 ∪ 𝑏) ∧ 𝑤 ∈ (𝑎 ∪ 𝑏))) → (𝐹‘𝑤) = if(𝑤 ∈ 𝑎, 〈𝑤, if(𝑤 = 𝑚, 𝑡, 𝑠)〉, 〈if(𝑤 = 𝑡, 𝑛, 𝑚), 𝑤〉)) |
38 | | iftrue 4042 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 ∈ 𝑎 → if(𝑤 ∈ 𝑎, 〈𝑤, if(𝑤 = 𝑚, 𝑡, 𝑠)〉, 〈if(𝑤 = 𝑡, 𝑛, 𝑚), 𝑤〉) = 〈𝑤, if(𝑤 = 𝑚, 𝑡, 𝑠)〉) |
39 | 38 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝑧 ∈ 𝑎 ∧ 𝑤 ∈ 𝑎) → if(𝑤 ∈ 𝑎, 〈𝑤, if(𝑤 = 𝑚, 𝑡, 𝑠)〉, 〈if(𝑤 = 𝑡, 𝑛, 𝑚), 𝑤〉) = 〈𝑤, if(𝑤 = 𝑚, 𝑡, 𝑠)〉) |
40 | 37, 39 | sylan9eq 2664 |
. . . . . . . . . . . . . 14
⊢ ((((¬
𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡) ∧ (𝑧 ∈ (𝑎 ∪ 𝑏) ∧ 𝑤 ∈ (𝑎 ∪ 𝑏))) ∧ (𝑧 ∈ 𝑎 ∧ 𝑤 ∈ 𝑎)) → (𝐹‘𝑤) = 〈𝑤, if(𝑤 = 𝑚, 𝑡, 𝑠)〉) |
41 | 35, 40 | eqeq12d 2625 |
. . . . . . . . . . . . 13
⊢ ((((¬
𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡) ∧ (𝑧 ∈ (𝑎 ∪ 𝑏) ∧ 𝑤 ∈ (𝑎 ∪ 𝑏))) ∧ (𝑧 ∈ 𝑎 ∧ 𝑤 ∈ 𝑎)) → ((𝐹‘𝑧) = (𝐹‘𝑤) ↔ 〈𝑧, if(𝑧 = 𝑚, 𝑡, 𝑠)〉 = 〈𝑤, if(𝑤 = 𝑚, 𝑡, 𝑠)〉)) |
42 | | vex 3176 |
. . . . . . . . . . . . . 14
⊢ 𝑧 ∈ V |
43 | | vex 3176 |
. . . . . . . . . . . . . . 15
⊢ 𝑡 ∈ V |
44 | | vex 3176 |
. . . . . . . . . . . . . . 15
⊢ 𝑠 ∈ V |
45 | 43, 44 | ifex 4106 |
. . . . . . . . . . . . . 14
⊢ if(𝑧 = 𝑚, 𝑡, 𝑠) ∈ V |
46 | 42, 45 | opth1 4870 |
. . . . . . . . . . . . 13
⊢
(〈𝑧, if(𝑧 = 𝑚, 𝑡, 𝑠)〉 = 〈𝑤, if(𝑤 = 𝑚, 𝑡, 𝑠)〉 → 𝑧 = 𝑤) |
47 | 41, 46 | syl6bi 242 |
. . . . . . . . . . . 12
⊢ ((((¬
𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡) ∧ (𝑧 ∈ (𝑎 ∪ 𝑏) ∧ 𝑤 ∈ (𝑎 ∪ 𝑏))) ∧ (𝑧 ∈ 𝑎 ∧ 𝑤 ∈ 𝑎)) → ((𝐹‘𝑧) = (𝐹‘𝑤) → 𝑧 = 𝑤)) |
48 | | simprr 792 |
. . . . . . . . . . . . . 14
⊢ (((¬
𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡) ∧ (𝑧 ∈ (𝑎 ∪ 𝑏) ∧ 𝑤 ∈ (𝑎 ∪ 𝑏))) → 𝑤 ∈ (𝑎 ∪ 𝑏)) |
49 | | simpll 786 |
. . . . . . . . . . . . . 14
⊢ (((¬
𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡) ∧ (𝑧 ∈ (𝑎 ∪ 𝑏) ∧ 𝑤 ∈ (𝑎 ∪ 𝑏))) → ¬ 𝑚 = 𝑛) |
50 | | simplr 788 |
. . . . . . . . . . . . . 14
⊢ (((¬
𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡) ∧ (𝑧 ∈ (𝑎 ∪ 𝑏) ∧ 𝑤 ∈ (𝑎 ∪ 𝑏))) → ¬ 𝑠 = 𝑡) |
51 | 29, 9, 48, 49, 50 | unxpdomlem2 8050 |
. . . . . . . . . . . . 13
⊢ ((((¬
𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡) ∧ (𝑧 ∈ (𝑎 ∪ 𝑏) ∧ 𝑤 ∈ (𝑎 ∪ 𝑏))) ∧ (𝑧 ∈ 𝑎 ∧ ¬ 𝑤 ∈ 𝑎)) → ¬ (𝐹‘𝑧) = (𝐹‘𝑤)) |
52 | 51 | pm2.21d 117 |
. . . . . . . . . . . 12
⊢ ((((¬
𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡) ∧ (𝑧 ∈ (𝑎 ∪ 𝑏) ∧ 𝑤 ∈ (𝑎 ∪ 𝑏))) ∧ (𝑧 ∈ 𝑎 ∧ ¬ 𝑤 ∈ 𝑎)) → ((𝐹‘𝑧) = (𝐹‘𝑤) → 𝑧 = 𝑤)) |
53 | | eqcom 2617 |
. . . . . . . . . . . . 13
⊢ ((𝐹‘𝑧) = (𝐹‘𝑤) ↔ (𝐹‘𝑤) = (𝐹‘𝑧)) |
54 | | simprl 790 |
. . . . . . . . . . . . . . . 16
⊢ (((¬
𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡) ∧ (𝑧 ∈ (𝑎 ∪ 𝑏) ∧ 𝑤 ∈ (𝑎 ∪ 𝑏))) → 𝑧 ∈ (𝑎 ∪ 𝑏)) |
55 | 29, 9, 54, 49, 50 | unxpdomlem2 8050 |
. . . . . . . . . . . . . . 15
⊢ ((((¬
𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡) ∧ (𝑧 ∈ (𝑎 ∪ 𝑏) ∧ 𝑤 ∈ (𝑎 ∪ 𝑏))) ∧ (𝑤 ∈ 𝑎 ∧ ¬ 𝑧 ∈ 𝑎)) → ¬ (𝐹‘𝑤) = (𝐹‘𝑧)) |
56 | 55 | ancom2s 840 |
. . . . . . . . . . . . . 14
⊢ ((((¬
𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡) ∧ (𝑧 ∈ (𝑎 ∪ 𝑏) ∧ 𝑤 ∈ (𝑎 ∪ 𝑏))) ∧ (¬ 𝑧 ∈ 𝑎 ∧ 𝑤 ∈ 𝑎)) → ¬ (𝐹‘𝑤) = (𝐹‘𝑧)) |
57 | 56 | pm2.21d 117 |
. . . . . . . . . . . . 13
⊢ ((((¬
𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡) ∧ (𝑧 ∈ (𝑎 ∪ 𝑏) ∧ 𝑤 ∈ (𝑎 ∪ 𝑏))) ∧ (¬ 𝑧 ∈ 𝑎 ∧ 𝑤 ∈ 𝑎)) → ((𝐹‘𝑤) = (𝐹‘𝑧) → 𝑧 = 𝑤)) |
58 | 53, 57 | syl5bi 231 |
. . . . . . . . . . . 12
⊢ ((((¬
𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡) ∧ (𝑧 ∈ (𝑎 ∪ 𝑏) ∧ 𝑤 ∈ (𝑎 ∪ 𝑏))) ∧ (¬ 𝑧 ∈ 𝑎 ∧ 𝑤 ∈ 𝑎)) → ((𝐹‘𝑧) = (𝐹‘𝑤) → 𝑧 = 𝑤)) |
59 | | iffalse 4045 |
. . . . . . . . . . . . . . . 16
⊢ (¬
𝑧 ∈ 𝑎 → if(𝑧 ∈ 𝑎, 〈𝑧, if(𝑧 = 𝑚, 𝑡, 𝑠)〉, 〈if(𝑧 = 𝑡, 𝑛, 𝑚), 𝑧〉) = 〈if(𝑧 = 𝑡, 𝑛, 𝑚), 𝑧〉) |
60 | 59 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((¬
𝑧 ∈ 𝑎 ∧ ¬ 𝑤 ∈ 𝑎) → if(𝑧 ∈ 𝑎, 〈𝑧, if(𝑧 = 𝑚, 𝑡, 𝑠)〉, 〈if(𝑧 = 𝑡, 𝑛, 𝑚), 𝑧〉) = 〈if(𝑧 = 𝑡, 𝑛, 𝑚), 𝑧〉) |
61 | 32, 60 | sylan9eq 2664 |
. . . . . . . . . . . . . 14
⊢ ((((¬
𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡) ∧ (𝑧 ∈ (𝑎 ∪ 𝑏) ∧ 𝑤 ∈ (𝑎 ∪ 𝑏))) ∧ (¬ 𝑧 ∈ 𝑎 ∧ ¬ 𝑤 ∈ 𝑎)) → (𝐹‘𝑧) = 〈if(𝑧 = 𝑡, 𝑛, 𝑚), 𝑧〉) |
62 | | iffalse 4045 |
. . . . . . . . . . . . . . . 16
⊢ (¬
𝑤 ∈ 𝑎 → if(𝑤 ∈ 𝑎, 〈𝑤, if(𝑤 = 𝑚, 𝑡, 𝑠)〉, 〈if(𝑤 = 𝑡, 𝑛, 𝑚), 𝑤〉) = 〈if(𝑤 = 𝑡, 𝑛, 𝑚), 𝑤〉) |
63 | 62 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((¬
𝑧 ∈ 𝑎 ∧ ¬ 𝑤 ∈ 𝑎) → if(𝑤 ∈ 𝑎, 〈𝑤, if(𝑤 = 𝑚, 𝑡, 𝑠)〉, 〈if(𝑤 = 𝑡, 𝑛, 𝑚), 𝑤〉) = 〈if(𝑤 = 𝑡, 𝑛, 𝑚), 𝑤〉) |
64 | 37, 63 | sylan9eq 2664 |
. . . . . . . . . . . . . 14
⊢ ((((¬
𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡) ∧ (𝑧 ∈ (𝑎 ∪ 𝑏) ∧ 𝑤 ∈ (𝑎 ∪ 𝑏))) ∧ (¬ 𝑧 ∈ 𝑎 ∧ ¬ 𝑤 ∈ 𝑎)) → (𝐹‘𝑤) = 〈if(𝑤 = 𝑡, 𝑛, 𝑚), 𝑤〉) |
65 | 61, 64 | eqeq12d 2625 |
. . . . . . . . . . . . 13
⊢ ((((¬
𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡) ∧ (𝑧 ∈ (𝑎 ∪ 𝑏) ∧ 𝑤 ∈ (𝑎 ∪ 𝑏))) ∧ (¬ 𝑧 ∈ 𝑎 ∧ ¬ 𝑤 ∈ 𝑎)) → ((𝐹‘𝑧) = (𝐹‘𝑤) ↔ 〈if(𝑧 = 𝑡, 𝑛, 𝑚), 𝑧〉 = 〈if(𝑤 = 𝑡, 𝑛, 𝑚), 𝑤〉)) |
66 | | vex 3176 |
. . . . . . . . . . . . . . . 16
⊢ 𝑛 ∈ V |
67 | | vex 3176 |
. . . . . . . . . . . . . . . 16
⊢ 𝑚 ∈ V |
68 | 66, 67 | ifex 4106 |
. . . . . . . . . . . . . . 15
⊢ if(𝑧 = 𝑡, 𝑛, 𝑚) ∈ V |
69 | 68, 42 | opth 4871 |
. . . . . . . . . . . . . 14
⊢
(〈if(𝑧 = 𝑡, 𝑛, 𝑚), 𝑧〉 = 〈if(𝑤 = 𝑡, 𝑛, 𝑚), 𝑤〉 ↔ (if(𝑧 = 𝑡, 𝑛, 𝑚) = if(𝑤 = 𝑡, 𝑛, 𝑚) ∧ 𝑧 = 𝑤)) |
70 | 69 | simprbi 479 |
. . . . . . . . . . . . 13
⊢
(〈if(𝑧 = 𝑡, 𝑛, 𝑚), 𝑧〉 = 〈if(𝑤 = 𝑡, 𝑛, 𝑚), 𝑤〉 → 𝑧 = 𝑤) |
71 | 65, 70 | syl6bi 242 |
. . . . . . . . . . . 12
⊢ ((((¬
𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡) ∧ (𝑧 ∈ (𝑎 ∪ 𝑏) ∧ 𝑤 ∈ (𝑎 ∪ 𝑏))) ∧ (¬ 𝑧 ∈ 𝑎 ∧ ¬ 𝑤 ∈ 𝑎)) → ((𝐹‘𝑧) = (𝐹‘𝑤) → 𝑧 = 𝑤)) |
72 | 47, 52, 58, 71 | 4casesdan 988 |
. . . . . . . . . . 11
⊢ (((¬
𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡) ∧ (𝑧 ∈ (𝑎 ∪ 𝑏) ∧ 𝑤 ∈ (𝑎 ∪ 𝑏))) → ((𝐹‘𝑧) = (𝐹‘𝑤) → 𝑧 = 𝑤)) |
73 | 72 | ralrimivva 2954 |
. . . . . . . . . 10
⊢ ((¬
𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡) → ∀𝑧 ∈ (𝑎 ∪ 𝑏)∀𝑤 ∈ (𝑎 ∪ 𝑏)((𝐹‘𝑧) = (𝐹‘𝑤) → 𝑧 = 𝑤)) |
74 | 73 | 3ad2ant3 1077 |
. . . . . . . . 9
⊢ (((𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏) ∧ (𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏) ∧ (¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡)) → ∀𝑧 ∈ (𝑎 ∪ 𝑏)∀𝑤 ∈ (𝑎 ∪ 𝑏)((𝐹‘𝑧) = (𝐹‘𝑤) → 𝑧 = 𝑤)) |
75 | | dff13 6416 |
. . . . . . . . 9
⊢ (𝐹:(𝑎 ∪ 𝑏)–1-1→(𝑎 × 𝑏) ↔ (𝐹:(𝑎 ∪ 𝑏)⟶(𝑎 × 𝑏) ∧ ∀𝑧 ∈ (𝑎 ∪ 𝑏)∀𝑤 ∈ (𝑎 ∪ 𝑏)((𝐹‘𝑧) = (𝐹‘𝑤) → 𝑧 = 𝑤))) |
76 | 30, 74, 75 | sylanbrc 695 |
. . . . . . . 8
⊢ (((𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏) ∧ (𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏) ∧ (¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡)) → 𝐹:(𝑎 ∪ 𝑏)–1-1→(𝑎 × 𝑏)) |
77 | 1, 4 | unex 6854 |
. . . . . . . . 9
⊢ (𝑎 ∪ 𝑏) ∈ V |
78 | 1, 4 | xpex 6860 |
. . . . . . . . 9
⊢ (𝑎 × 𝑏) ∈ V |
79 | | f1dom2g 7859 |
. . . . . . . . 9
⊢ (((𝑎 ∪ 𝑏) ∈ V ∧ (𝑎 × 𝑏) ∈ V ∧ 𝐹:(𝑎 ∪ 𝑏)–1-1→(𝑎 × 𝑏)) → (𝑎 ∪ 𝑏) ≼ (𝑎 × 𝑏)) |
80 | 77, 78, 79 | mp3an12 1406 |
. . . . . . . 8
⊢ (𝐹:(𝑎 ∪ 𝑏)–1-1→(𝑎 × 𝑏) → (𝑎 ∪ 𝑏) ≼ (𝑎 × 𝑏)) |
81 | 76, 80 | syl 17 |
. . . . . . 7
⊢ (((𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏) ∧ (𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏) ∧ (¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡)) → (𝑎 ∪ 𝑏) ≼ (𝑎 × 𝑏)) |
82 | 81 | 3expia 1259 |
. . . . . 6
⊢ (((𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏) ∧ (𝑛 ∈ 𝑎 ∧ 𝑡 ∈ 𝑏)) → ((¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡) → (𝑎 ∪ 𝑏) ≼ (𝑎 × 𝑏))) |
83 | 82 | rexlimdvva 3020 |
. . . . 5
⊢ ((𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏) → (∃𝑛 ∈ 𝑎 ∃𝑡 ∈ 𝑏 (¬ 𝑚 = 𝑛 ∧ ¬ 𝑠 = 𝑡) → (𝑎 ∪ 𝑏) ≼ (𝑎 × 𝑏))) |
84 | 8, 83 | syl5bir 232 |
. . . 4
⊢ ((𝑚 ∈ 𝑎 ∧ 𝑠 ∈ 𝑏) → ((∃𝑛 ∈ 𝑎 ¬ 𝑚 = 𝑛 ∧ ∃𝑡 ∈ 𝑏 ¬ 𝑠 = 𝑡) → (𝑎 ∪ 𝑏) ≼ (𝑎 × 𝑏))) |
85 | 84 | rexlimivv 3018 |
. . 3
⊢
(∃𝑚 ∈
𝑎 ∃𝑠 ∈ 𝑏 (∃𝑛 ∈ 𝑎 ¬ 𝑚 = 𝑛 ∧ ∃𝑡 ∈ 𝑏 ¬ 𝑠 = 𝑡) → (𝑎 ∪ 𝑏) ≼ (𝑎 × 𝑏)) |
86 | 7, 85 | sylbir 224 |
. 2
⊢
((∃𝑚 ∈
𝑎 ∃𝑛 ∈ 𝑎 ¬ 𝑚 = 𝑛 ∧ ∃𝑠 ∈ 𝑏 ∃𝑡 ∈ 𝑏 ¬ 𝑠 = 𝑡) → (𝑎 ∪ 𝑏) ≼ (𝑎 × 𝑏)) |
87 | 3, 6, 86 | syl2anb 495 |
1
⊢
((1𝑜 ≺ 𝑎 ∧ 1𝑜 ≺ 𝑏) → (𝑎 ∪ 𝑏) ≼ (𝑎 × 𝑏)) |