Metamath Proof Explorer

Theorem soinfdom

Description: A strict order relation on an infinite set dominates that set. (Contributed by BTernaryTau, 14-Jul-2026)

Ref Expression
Assertion soinfdom ( ( 𝑅 Or 𝐴 ∧ 𝑅 ∈ 𝑉 ∧ ω ≼ 𝐴 ) → 𝐴 ≼ 𝑅 )

Proof

Step Hyp Ref Expression
1 infn0 ⊢ ( ω ≼ 𝐴 → 𝐴 ≠ ∅ )
2 n0 ⊢ ( 𝐴 ≠ ∅ ↔ ∃ 𝑦 𝑦 ∈ 𝐴 )
3 1 2 sylib ⊢ ( ω ≼ 𝐴 → ∃ 𝑦 𝑦 ∈ 𝐴 )
4 3 adantr ⊢ ( ( ω ≼ 𝐴 ∧ ( 𝑅 ∈ 𝑉 ∧ 𝑅 Or 𝐴 ) ) → ∃ 𝑦 𝑦 ∈ 𝐴 )
5 infdifsn ⊢ ( ω ≼ 𝐴 → ( 𝐴 ∖ { 𝑦 } ) ≈ 𝐴 )
6 5 ensymd ⊢ ( ω ≼ 𝐴 → 𝐴 ≈ ( 𝐴 ∖ { 𝑦 } ) )
7 eldifsn ⊢ ( 𝑧 ∈ ( 𝐴 ∖ { 𝑦 } ) ↔ ( 𝑧 ∈ 𝐴 ∧ 𝑧 ≠ 𝑦 ) )
8 sotrine ⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( 𝑧 ≠ 𝑦 ↔ ( 𝑧 𝑅 𝑦 ∨ 𝑦 𝑅 𝑧 ) ) )
9 8 biimpd ⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( 𝑧 ≠ 𝑦 → ( 𝑧 𝑅 𝑦 ∨ 𝑦 𝑅 𝑧 ) ) )
10 9 ancom2s ⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) → ( 𝑧 ≠ 𝑦 → ( 𝑧 𝑅 𝑦 ∨ 𝑦 𝑅 𝑧 ) ) )
11 10 expr ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑧 ∈ 𝐴 → ( 𝑧 ≠ 𝑦 → ( 𝑧 𝑅 𝑦 ∨ 𝑦 𝑅 𝑧 ) ) ) )
12 11 impd ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝑧 ∈ 𝐴 ∧ 𝑧 ≠ 𝑦 ) → ( 𝑧 𝑅 𝑦 ∨ 𝑦 𝑅 𝑧 ) ) )
13 7 12 biimtrid ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑧 ∈ ( 𝐴 ∖ { 𝑦 } ) → ( 𝑧 𝑅 𝑦 ∨ 𝑦 𝑅 𝑧 ) ) )
14 iftrue ⊢ ( 𝑧 𝑅 𝑦 → if ( 𝑧 𝑅 𝑦 , ⟨ 𝑧 , 𝑦 ⟩ , ⟨ 𝑦 , 𝑧 ⟩ ) = ⟨ 𝑧 , 𝑦 ⟩ )
15 df-br ⊢ ( 𝑧 𝑅 𝑦 ↔ ⟨ 𝑧 , 𝑦 ⟩ ∈ 𝑅 )
16 15 biimpi ⊢ ( 𝑧 𝑅 𝑦 → ⟨ 𝑧 , 𝑦 ⟩ ∈ 𝑅 )
17 14 16 eqeltrd ⊢ ( 𝑧 𝑅 𝑦 → if ( 𝑧 𝑅 𝑦 , ⟨ 𝑧 , 𝑦 ⟩ , ⟨ 𝑦 , 𝑧 ⟩ ) ∈ 𝑅 )
18 df-br ⊢ ( 𝑦 𝑅 𝑧 ↔ ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝑅 )
19 18 bilani ⊢ ( ( ¬ 𝑧 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝑅 )
20 iffalse ⊢ ( ¬ 𝑧 𝑅 𝑦 → if ( 𝑧 𝑅 𝑦 , ⟨ 𝑧 , 𝑦 ⟩ , ⟨ 𝑦 , 𝑧 ⟩ ) = ⟨ 𝑦 , 𝑧 ⟩ )
21 20 eleq1d ⊢ ( ¬ 𝑧 𝑅 𝑦 → ( if ( 𝑧 𝑅 𝑦 , ⟨ 𝑧 , 𝑦 ⟩ , ⟨ 𝑦 , 𝑧 ⟩ ) ∈ 𝑅 ↔ ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝑅 ) )
22 21 adantr ⊢ ( ( ¬ 𝑧 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → ( if ( 𝑧 𝑅 𝑦 , ⟨ 𝑧 , 𝑦 ⟩ , ⟨ 𝑦 , 𝑧 ⟩ ) ∈ 𝑅 ↔ ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝑅 ) )
23 19 22 mpbird ⊢ ( ( ¬ 𝑧 𝑅 𝑦 ∧ 𝑦 𝑅 𝑧 ) → if ( 𝑧 𝑅 𝑦 , ⟨ 𝑧 , 𝑦 ⟩ , ⟨ 𝑦 , 𝑧 ⟩ ) ∈ 𝑅 )
24 17 23 jaoi3 ⊢ ( ( 𝑧 𝑅 𝑦 ∨ 𝑦 𝑅 𝑧 ) → if ( 𝑧 𝑅 𝑦 , ⟨ 𝑧 , 𝑦 ⟩ , ⟨ 𝑦 , 𝑧 ⟩ ) ∈ 𝑅 )
25 13 24 syl6 ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑧 ∈ ( 𝐴 ∖ { 𝑦 } ) → if ( 𝑧 𝑅 𝑦 , ⟨ 𝑧 , 𝑦 ⟩ , ⟨ 𝑦 , 𝑧 ⟩ ) ∈ 𝑅 ) )
26 25 ralrimiv ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ∀ 𝑧 ∈ ( 𝐴 ∖ { 𝑦 } ) if ( 𝑧 𝑅 𝑦 , ⟨ 𝑧 , 𝑦 ⟩ , ⟨ 𝑦 , 𝑧 ⟩ ) ∈ 𝑅 )
27 eldifsnneq ⊢ ( 𝑤 ∈ ( 𝐴 ∖ { 𝑦 } ) → ¬ 𝑤 = 𝑦 )
28 27 neqcomd ⊢ ( 𝑤 ∈ ( 𝐴 ∖ { 𝑦 } ) → ¬ 𝑦 = 𝑤 )
29 vex ⊢ 𝑧 ∈ V
30 vex ⊢ 𝑦 ∈ V
31 29 30 opth1 ⊢ ( ⟨ 𝑧 , 𝑦 ⟩ = ⟨ 𝑤 , 𝑦 ⟩ → 𝑧 = 𝑤 )
32 31 a1d ⊢ ( ⟨ 𝑧 , 𝑦 ⟩ = ⟨ 𝑤 , 𝑦 ⟩ → ( ¬ 𝑦 = 𝑤 → 𝑧 = 𝑤 ) )
33 29 30 opth ⊢ ( ⟨ 𝑧 , 𝑦 ⟩ = ⟨ 𝑦 , 𝑤 ⟩ ↔ ( 𝑧 = 𝑦 ∧ 𝑦 = 𝑤 ) )
34 33 simprbi ⊢ ( ⟨ 𝑧 , 𝑦 ⟩ = ⟨ 𝑦 , 𝑤 ⟩ → 𝑦 = 𝑤 )
35 34 pm2.24d ⊢ ( ⟨ 𝑧 , 𝑦 ⟩ = ⟨ 𝑦 , 𝑤 ⟩ → ( ¬ 𝑦 = 𝑤 → 𝑧 = 𝑤 ) )
36 30 29 opth1 ⊢ ( ⟨ 𝑦 , 𝑧 ⟩ = ⟨ 𝑤 , 𝑦 ⟩ → 𝑦 = 𝑤 )
37 36 pm2.24d ⊢ ( ⟨ 𝑦 , 𝑧 ⟩ = ⟨ 𝑤 , 𝑦 ⟩ → ( ¬ 𝑦 = 𝑤 → 𝑧 = 𝑤 ) )
38 30 29 opth ⊢ ( ⟨ 𝑦 , 𝑧 ⟩ = ⟨ 𝑦 , 𝑤 ⟩ ↔ ( 𝑦 = 𝑦 ∧ 𝑧 = 𝑤 ) )
39 38 simprbi ⊢ ( ⟨ 𝑦 , 𝑧 ⟩ = ⟨ 𝑦 , 𝑤 ⟩ → 𝑧 = 𝑤 )
40 39 a1d ⊢ ( ⟨ 𝑦 , 𝑧 ⟩ = ⟨ 𝑦 , 𝑤 ⟩ → ( ¬ 𝑦 = 𝑤 → 𝑧 = 𝑤 ) )
41 32 35 37 40 jaeqifi ⊢ ( if ( 𝑧 𝑅 𝑦 , ⟨ 𝑧 , 𝑦 ⟩ , ⟨ 𝑦 , 𝑧 ⟩ ) = if ( 𝑤 𝑅 𝑦 , ⟨ 𝑤 , 𝑦 ⟩ , ⟨ 𝑦 , 𝑤 ⟩ ) → ( ¬ 𝑦 = 𝑤 → 𝑧 = 𝑤 ) )
42 28 41 syl5com ⊢ ( 𝑤 ∈ ( 𝐴 ∖ { 𝑦 } ) → ( if ( 𝑧 𝑅 𝑦 , ⟨ 𝑧 , 𝑦 ⟩ , ⟨ 𝑦 , 𝑧 ⟩ ) = if ( 𝑤 𝑅 𝑦 , ⟨ 𝑤 , 𝑦 ⟩ , ⟨ 𝑦 , 𝑤 ⟩ ) → 𝑧 = 𝑤 ) )
43 42 rgen ⊢ ∀ 𝑤 ∈ ( 𝐴 ∖ { 𝑦 } ) ( if ( 𝑧 𝑅 𝑦 , ⟨ 𝑧 , 𝑦 ⟩ , ⟨ 𝑦 , 𝑧 ⟩ ) = if ( 𝑤 𝑅 𝑦 , ⟨ 𝑤 , 𝑦 ⟩ , ⟨ 𝑦 , 𝑤 ⟩ ) → 𝑧 = 𝑤 )
44 43 rgenw ⊢ ∀ 𝑧 ∈ ( 𝐴 ∖ { 𝑦 } ) ∀ 𝑤 ∈ ( 𝐴 ∖ { 𝑦 } ) ( if ( 𝑧 𝑅 𝑦 , ⟨ 𝑧 , 𝑦 ⟩ , ⟨ 𝑦 , 𝑧 ⟩ ) = if ( 𝑤 𝑅 𝑦 , ⟨ 𝑤 , 𝑦 ⟩ , ⟨ 𝑦 , 𝑤 ⟩ ) → 𝑧 = 𝑤 )
45 eqid ⊢ ( 𝑧 ∈ ( 𝐴 ∖ { 𝑦 } ) ↦ if ( 𝑧 𝑅 𝑦 , ⟨ 𝑧 , 𝑦 ⟩ , ⟨ 𝑦 , 𝑧 ⟩ ) ) = ( 𝑧 ∈ ( 𝐴 ∖ { 𝑦 } ) ↦ if ( 𝑧 𝑅 𝑦 , ⟨ 𝑧 , 𝑦 ⟩ , ⟨ 𝑦 , 𝑧 ⟩ ) )
46 breq1 ⊢ ( 𝑧 = 𝑤 → ( 𝑧 𝑅 𝑦 ↔ 𝑤 𝑅 𝑦 ) )
47 opeq1 ⊢ ( 𝑧 = 𝑤 → ⟨ 𝑧 , 𝑦 ⟩ = ⟨ 𝑤 , 𝑦 ⟩ )
48 opeq2 ⊢ ( 𝑧 = 𝑤 → ⟨ 𝑦 , 𝑧 ⟩ = ⟨ 𝑦 , 𝑤 ⟩ )
49 46 47 48 ifbieq12d ⊢ ( 𝑧 = 𝑤 → if ( 𝑧 𝑅 𝑦 , ⟨ 𝑧 , 𝑦 ⟩ , ⟨ 𝑦 , 𝑧 ⟩ ) = if ( 𝑤 𝑅 𝑦 , ⟨ 𝑤 , 𝑦 ⟩ , ⟨ 𝑦 , 𝑤 ⟩ ) )
50 45 49 f1mpt ⊢ ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝑦 } ) ↦ if ( 𝑧 𝑅 𝑦 , ⟨ 𝑧 , 𝑦 ⟩ , ⟨ 𝑦 , 𝑧 ⟩ ) ) : ( 𝐴 ∖ { 𝑦 } ) –1-1→ 𝑅 ↔ ( ∀ 𝑧 ∈ ( 𝐴 ∖ { 𝑦 } ) if ( 𝑧 𝑅 𝑦 , ⟨ 𝑧 , 𝑦 ⟩ , ⟨ 𝑦 , 𝑧 ⟩ ) ∈ 𝑅 ∧ ∀ 𝑧 ∈ ( 𝐴 ∖ { 𝑦 } ) ∀ 𝑤 ∈ ( 𝐴 ∖ { 𝑦 } ) ( if ( 𝑧 𝑅 𝑦 , ⟨ 𝑧 , 𝑦 ⟩ , ⟨ 𝑦 , 𝑧 ⟩ ) = if ( 𝑤 𝑅 𝑦 , ⟨ 𝑤 , 𝑦 ⟩ , ⟨ 𝑦 , 𝑤 ⟩ ) → 𝑧 = 𝑤 ) ) )
51 26 44 50 sylanblrc ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑧 ∈ ( 𝐴 ∖ { 𝑦 } ) ↦ if ( 𝑧 𝑅 𝑦 , ⟨ 𝑧 , 𝑦 ⟩ , ⟨ 𝑦 , 𝑧 ⟩ ) ) : ( 𝐴 ∖ { 𝑦 } ) –1-1→ 𝑅 )
52 f1domg ⊢ ( 𝑅 ∈ 𝑉 → ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝑦 } ) ↦ if ( 𝑧 𝑅 𝑦 , ⟨ 𝑧 , 𝑦 ⟩ , ⟨ 𝑦 , 𝑧 ⟩ ) ) : ( 𝐴 ∖ { 𝑦 } ) –1-1→ 𝑅 → ( 𝐴 ∖ { 𝑦 } ) ≼ 𝑅 ) )
53 51 52 syl5 ⊢ ( 𝑅 ∈ 𝑉 → ( ( 𝑅 Or 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝐴 ∖ { 𝑦 } ) ≼ 𝑅 ) )
54 53 impl ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑅 Or 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝐴 ∖ { 𝑦 } ) ≼ 𝑅 )
55 endomtr ⊢ ( ( 𝐴 ≈ ( 𝐴 ∖ { 𝑦 } ) ∧ ( 𝐴 ∖ { 𝑦 } ) ≼ 𝑅 ) → 𝐴 ≼ 𝑅 )
56 6 54 55 syl3an132 ⊢ ( ( ω ≼ 𝐴 ∧ ( 𝑅 ∈ 𝑉 ∧ 𝑅 Or 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → 𝐴 ≼ 𝑅 )
57 56 3expia ⊢ ( ( ω ≼ 𝐴 ∧ ( 𝑅 ∈ 𝑉 ∧ 𝑅 Or 𝐴 ) ) → ( 𝑦 ∈ 𝐴 → 𝐴 ≼ 𝑅 ) )
58 57 exlimdv ⊢ ( ( ω ≼ 𝐴 ∧ ( 𝑅 ∈ 𝑉 ∧ 𝑅 Or 𝐴 ) ) → ( ∃ 𝑦 𝑦 ∈ 𝐴 → 𝐴 ≼ 𝑅 ) )
59 4 58 mpd ⊢ ( ( ω ≼ 𝐴 ∧ ( 𝑅 ∈ 𝑉 ∧ 𝑅 Or 𝐴 ) ) → 𝐴 ≼ 𝑅 )
60 59 ancom2s ⊢ ( ( ω ≼ 𝐴 ∧ ( 𝑅 Or 𝐴 ∧ 𝑅 ∈ 𝑉 ) ) → 𝐴 ≼ 𝑅 )
61 60 ancoms ⊢ ( ( ( 𝑅 Or 𝐴 ∧ 𝑅 ∈ 𝑉 ) ∧ ω ≼ 𝐴 ) → 𝐴 ≼ 𝑅 )
62 61 3impa ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝑅 ∈ 𝑉 ∧ ω ≼ 𝐴 ) → 𝐴 ≼ 𝑅 )