Metamath Proof Explorer


Theorem 1sdom2dom

Description: Strict dominance over 1 is the same as dominance over 2. (Contributed by BTernaryTau, 23-Dec-2024)

Ref Expression
Assertion 1sdom2dom ( 1o𝐴 ↔ 2o𝐴 )

Proof

Step Hyp Ref Expression
1 relsdom Rel ≺
2 1 brrelex2i ( 1o𝐴𝐴 ∈ V )
3 sdomdom ( 1o𝐴 → 1o𝐴 )
4 0sdom1dom ( ∅ ≺ 𝐴 ↔ 1o𝐴 )
5 3 4 sylibr ( 1o𝐴 → ∅ ≺ 𝐴 )
6 0sdomg ( 𝐴 ∈ V → ( ∅ ≺ 𝐴𝐴 ≠ ∅ ) )
7 2 6 syl ( 1o𝐴 → ( ∅ ≺ 𝐴𝐴 ≠ ∅ ) )
8 5 7 mpbid ( 1o𝐴𝐴 ≠ ∅ )
9 n0snor2el ( 𝐴 ≠ ∅ → ( ∃ 𝑥𝐴𝑦𝐴 𝑥𝑦 ∨ ∃ 𝑥 𝐴 = { 𝑥 } ) )
10 8 9 syl ( 1o𝐴 → ( ∃ 𝑥𝐴𝑦𝐴 𝑥𝑦 ∨ ∃ 𝑥 𝐴 = { 𝑥 } ) )
11 sdomnen ( 1o𝐴 → ¬ 1o𝐴 )
12 df1o2 1o = { ∅ }
13 0ex ∅ ∈ V
14 vex 𝑥 ∈ V
15 en2sn ( ( ∅ ∈ V ∧ 𝑥 ∈ V ) → { ∅ } ≈ { 𝑥 } )
16 13 14 15 mp2an { ∅ } ≈ { 𝑥 }
17 12 16 eqbrtri 1o ≈ { 𝑥 }
18 breq2 ( 𝐴 = { 𝑥 } → ( 1o𝐴 ↔ 1o ≈ { 𝑥 } ) )
19 17 18 mpbiri ( 𝐴 = { 𝑥 } → 1o𝐴 )
20 19 exlimiv ( ∃ 𝑥 𝐴 = { 𝑥 } → 1o𝐴 )
21 11 20 nsyl ( 1o𝐴 → ¬ ∃ 𝑥 𝐴 = { 𝑥 } )
22 10 21 olcnd ( 1o𝐴 → ∃ 𝑥𝐴𝑦𝐴 𝑥𝑦 )
23 rex2dom ( ( 𝐴 ∈ V ∧ ∃ 𝑥𝐴𝑦𝐴 𝑥𝑦 ) → 2o𝐴 )
24 2 22 23 syl2anc ( 1o𝐴 → 2o𝐴 )
25 snsspr1 { ∅ } ⊆ { ∅ , 1o }
26 df2o3 2o = { ∅ , 1o }
27 25 12 26 3sstr4i 1o ⊆ 2o
28 domssl ( ( 1o ⊆ 2o ∧ 2o𝐴 ) → 1o𝐴 )
29 27 28 mpan ( 2o𝐴 → 1o𝐴 )
30 snnen2o ¬ { 𝑦 } ≈ 2o
31 13 a1i ( ⊤ → ∅ ∈ V )
32 1oex 1o ∈ V
33 32 a1i ( ⊤ → 1o ∈ V )
34 1n0 1o ≠ ∅
35 34 nesymi ¬ ∅ = 1o
36 35 a1i ( ⊤ → ¬ ∅ = 1o )
37 31 33 36 enpr2d ( ⊤ → { ∅ , 1o } ≈ 2o )
38 37 mptru { ∅ , 1o } ≈ 2o
39 26 38 eqbrtri 2o ≈ 2o
40 breq1 ( 2o = { 𝑦 } → ( 2o ≈ 2o ↔ { 𝑦 } ≈ 2o ) )
41 39 40 mpbii ( 2o = { 𝑦 } → { 𝑦 } ≈ 2o )
42 30 41 mto ¬ 2o = { 𝑦 }
43 42 nex ¬ ∃ 𝑦 2o = { 𝑦 }
44 2on0 2o ≠ ∅
45 f1cdmsn ( ( 𝑓 : 2o1-1→ { 𝑥 } ∧ 2o ≠ ∅ ) → ∃ 𝑦 2o = { 𝑦 } )
46 44 45 mpan2 ( 𝑓 : 2o1-1→ { 𝑥 } → ∃ 𝑦 2o = { 𝑦 } )
47 43 46 mto ¬ 𝑓 : 2o1-1→ { 𝑥 }
48 47 nex ¬ ∃ 𝑓 𝑓 : 2o1-1→ { 𝑥 }
49 brdomi ( 2o ≼ { 𝑥 } → ∃ 𝑓 𝑓 : 2o1-1→ { 𝑥 } )
50 48 49 mto ¬ 2o ≼ { 𝑥 }
51 breq2 ( 𝐴 = { 𝑥 } → ( 2o𝐴 ↔ 2o ≼ { 𝑥 } ) )
52 50 51 mtbiri ( 𝐴 = { 𝑥 } → ¬ 2o𝐴 )
53 52 con2i ( 2o𝐴 → ¬ 𝐴 = { 𝑥 } )
54 53 nexdv ( 2o𝐴 → ¬ ∃ 𝑥 𝐴 = { 𝑥 } )
55 reldom Rel ≼
56 55 brrelex2i ( 2o𝐴𝐴 ∈ V )
57 breng ( ( 1o ∈ V ∧ 𝐴 ∈ V ) → ( 1o𝐴 ↔ ∃ 𝑓 𝑓 : 1o1-1-onto𝐴 ) )
58 32 57 mpan ( 𝐴 ∈ V → ( 1o𝐴 ↔ ∃ 𝑓 𝑓 : 1o1-1-onto𝐴 ) )
59 56 58 syl ( 2o𝐴 → ( 1o𝐴 ↔ ∃ 𝑓 𝑓 : 1o1-1-onto𝐴 ) )
60 29 4 sylibr ( 2o𝐴 → ∅ ≺ 𝐴 )
61 56 6 syl ( 2o𝐴 → ( ∅ ≺ 𝐴𝐴 ≠ ∅ ) )
62 60 61 mpbid ( 2o𝐴𝐴 ≠ ∅ )
63 f1ocnv ( 𝑓 : 1o1-1-onto𝐴 𝑓 : 𝐴1-1-onto→ 1o )
64 f1of1 ( 𝑓 : 𝐴1-1-onto→ 1o 𝑓 : 𝐴1-1→ 1o )
65 f1eq3 ( 1o = { ∅ } → ( 𝑓 : 𝐴1-1→ 1o 𝑓 : 𝐴1-1→ { ∅ } ) )
66 12 65 ax-mp ( 𝑓 : 𝐴1-1→ 1o 𝑓 : 𝐴1-1→ { ∅ } )
67 64 66 sylib ( 𝑓 : 𝐴1-1-onto→ 1o 𝑓 : 𝐴1-1→ { ∅ } )
68 63 67 syl ( 𝑓 : 1o1-1-onto𝐴 𝑓 : 𝐴1-1→ { ∅ } )
69 f1cdmsn ( ( 𝑓 : 𝐴1-1→ { ∅ } ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥 𝐴 = { 𝑥 } )
70 68 69 sylan ( ( 𝑓 : 1o1-1-onto𝐴𝐴 ≠ ∅ ) → ∃ 𝑥 𝐴 = { 𝑥 } )
71 70 expcom ( 𝐴 ≠ ∅ → ( 𝑓 : 1o1-1-onto𝐴 → ∃ 𝑥 𝐴 = { 𝑥 } ) )
72 71 exlimdv ( 𝐴 ≠ ∅ → ( ∃ 𝑓 𝑓 : 1o1-1-onto𝐴 → ∃ 𝑥 𝐴 = { 𝑥 } ) )
73 62 72 syl ( 2o𝐴 → ( ∃ 𝑓 𝑓 : 1o1-1-onto𝐴 → ∃ 𝑥 𝐴 = { 𝑥 } ) )
74 59 73 sylbid ( 2o𝐴 → ( 1o𝐴 → ∃ 𝑥 𝐴 = { 𝑥 } ) )
75 54 74 mtod ( 2o𝐴 → ¬ 1o𝐴 )
76 brsdom ( 1o𝐴 ↔ ( 1o𝐴 ∧ ¬ 1o𝐴 ) )
77 29 75 76 sylanbrc ( 2o𝐴 → 1o𝐴 )
78 24 77 impbii ( 1o𝐴 ↔ 2o𝐴 )