This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( ( 𝑓 : 2o –1-1→ { 𝑥 } ∧ 2o ≠ ∅ ) → ∃ 𝑦 2o = { 𝑦 } )
46 44 45 mpan2 ⊢ ( 𝑓 : 2o –1-1→ { 𝑥 } → ∃ 𝑦 2o = { 𝑦 } )
47 43 46 mto ⊢ ¬ 𝑓 : 2o –1-1→ { 𝑥 }
48 47 nex ⊢ ¬ ∃ 𝑓 𝑓 : 2o –1-1→ { 𝑥 }
49 brdomi ⊢ ( 2o ≼ { 𝑥 } → ∃ 𝑓 𝑓 : 2o –1-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 ≈ 𝐴 ↔ ∃ 𝑓 𝑓 : 1o –1-1-onto→ 𝐴 ) )
58 32 57 mpan ⊢ ( 𝐴 ∈ V → ( 1o ≈ 𝐴 ↔ ∃ 𝑓 𝑓 : 1o –1-1-onto→ 𝐴 ) )
59 56 58 syl ⊢ ( 2o ≼ 𝐴 → ( 1o ≈ 𝐴 ↔ ∃ 𝑓 𝑓 : 1o –1-1-onto→ 𝐴 ) )
60 29 4 sylibr ⊢ ( 2o ≼ 𝐴 → ∅ ≺ 𝐴 )
61 56 6 syl ⊢ ( 2o ≼ 𝐴 → ( ∅ ≺ 𝐴 ↔ 𝐴 ≠ ∅ ) )
62 60 61 mpbid ⊢ ( 2o ≼ 𝐴 → 𝐴 ≠ ∅ )
63 f1ocnv ⊢ ( 𝑓 : 1o –1-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 ⊢ ( 𝑓 : 1o –1-1-onto→ 𝐴 → ◡ 𝑓 : 𝐴 –1-1→ { ∅ } )
69 f1cdmsn ⊢ ( ( ◡ 𝑓 : 𝐴 –1-1→ { ∅ } ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥 𝐴 = { 𝑥 } )
70 68 69 sylan ⊢ ( ( 𝑓 : 1o –1-1-onto→ 𝐴 ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥 𝐴 = { 𝑥 } )
71 70 expcom ⊢ ( 𝐴 ≠ ∅ → ( 𝑓 : 1o –1-1-onto→ 𝐴 → ∃ 𝑥 𝐴 = { 𝑥 } ) )
72 71 exlimdv ⊢ ( 𝐴 ≠ ∅ → ( ∃ 𝑓 𝑓 : 1o –1-1-onto→ 𝐴 → ∃ 𝑥 𝐴 = { 𝑥 } ) )
73 62 72 syl ⊢ ( 2o ≼ 𝐴 → ( ∃ 𝑓 𝑓 : 1o –1-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 ≼ 𝐴 )