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 
|- ( ( R Or A /\ R e. V /\ _om ~<_ A ) -> A ~<_ R )

Proof

Step Hyp Ref Expression
1 infn0 
 |-  ( _om ~<_ A -> A =/= (/) )
2 n0 
 |-  ( A =/= (/) <-> E. y y e. A )
3 1 2 sylib 
 |-  ( _om ~<_ A -> E. y y e. A )
4 3 adantr 
 |-  ( ( _om ~<_ A /\ ( R e. V /\ R Or A ) ) -> E. y y e. A )
5 infdifsn 
 |-  ( _om ~<_ A -> ( A \ { y } ) ~~ A )
6 5 ensymd 
 |-  ( _om ~<_ A -> A ~~ ( A \ { y } ) )
7 eldifsn 
 |-  ( z e. ( A \ { y } ) <-> ( z e. A /\ z =/= y ) )
8 sotrine 
 |-  ( ( R Or A /\ ( z e. A /\ y e. A ) ) -> ( z =/= y <-> ( z R y \/ y R z ) ) )
9 8 biimpd 
 |-  ( ( R Or A /\ ( z e. A /\ y e. A ) ) -> ( z =/= y -> ( z R y \/ y R z ) ) )
10 9 ancom2s 
 |-  ( ( R Or A /\ ( y e. A /\ z e. A ) ) -> ( z =/= y -> ( z R y \/ y R z ) ) )
11 10 expr 
 |-  ( ( R Or A /\ y e. A ) -> ( z e. A -> ( z =/= y -> ( z R y \/ y R z ) ) ) )
12 11 impd 
 |-  ( ( R Or A /\ y e. A ) -> ( ( z e. A /\ z =/= y ) -> ( z R y \/ y R z ) ) )
13 7 12 biimtrid 
 |-  ( ( R Or A /\ y e. A ) -> ( z e. ( A \ { y } ) -> ( z R y \/ y R z ) ) )
14 iftrue 
 |-  ( z R y -> if ( z R y , <. z , y >. , <. y , z >. ) = <. z , y >. )
15 df-br 
 |-  ( z R y <-> <. z , y >. e. R )
16 15 biimpi 
 |-  ( z R y -> <. z , y >. e. R )
17 14 16 eqeltrd 
 |-  ( z R y -> if ( z R y , <. z , y >. , <. y , z >. ) e. R )
18 df-br 
 |-  ( y R z <-> <. y , z >. e. R )
19 18 bilani 
 |-  ( ( -. z R y /\ y R z ) -> <. y , z >. e. R )
20 iffalse 
 |-  ( -. z R y -> if ( z R y , <. z , y >. , <. y , z >. ) = <. y , z >. )
21 20 eleq1d 
 |-  ( -. z R y -> ( if ( z R y , <. z , y >. , <. y , z >. ) e. R <-> <. y , z >. e. R ) )
22 21 adantr 
 |-  ( ( -. z R y /\ y R z ) -> ( if ( z R y , <. z , y >. , <. y , z >. ) e. R <-> <. y , z >. e. R ) )
23 19 22 mpbird 
 |-  ( ( -. z R y /\ y R z ) -> if ( z R y , <. z , y >. , <. y , z >. ) e. R )
24 17 23 jaoi3 
 |-  ( ( z R y \/ y R z ) -> if ( z R y , <. z , y >. , <. y , z >. ) e. R )
25 13 24 syl6 
 |-  ( ( R Or A /\ y e. A ) -> ( z e. ( A \ { y } ) -> if ( z R y , <. z , y >. , <. y , z >. ) e. R ) )
26 25 ralrimiv 
 |-  ( ( R Or A /\ y e. A ) -> A. z e. ( A \ { y } ) if ( z R y , <. z , y >. , <. y , z >. ) e. R )
27 eldifsnneq 
 |-  ( w e. ( A \ { y } ) -> -. w = y )
28 27 neqcomd 
 |-  ( w e. ( A \ { y } ) -> -. y = w )
29 vex 
 |-  z e. _V
30 vex 
 |-  y e. _V
31 29 30 opth1 
 |-  ( <. z , y >. = <. w , y >. -> z = w )
32 31 a1d 
 |-  ( <. z , y >. = <. w , y >. -> ( -. y = w -> z = w ) )
33 29 30 opth 
 |-  ( <. z , y >. = <. y , w >. <-> ( z = y /\ y = w ) )
34 33 simprbi 
 |-  ( <. z , y >. = <. y , w >. -> y = w )
35 34 pm2.24d 
 |-  ( <. z , y >. = <. y , w >. -> ( -. y = w -> z = w ) )
36 30 29 opth1 
 |-  ( <. y , z >. = <. w , y >. -> y = w )
37 36 pm2.24d 
 |-  ( <. y , z >. = <. w , y >. -> ( -. y = w -> z = w ) )
38 30 29 opth 
 |-  ( <. y , z >. = <. y , w >. <-> ( y = y /\ z = w ) )
39 38 simprbi 
 |-  ( <. y , z >. = <. y , w >. -> z = w )
40 39 a1d 
 |-  ( <. y , z >. = <. y , w >. -> ( -. y = w -> z = w ) )
41 32 35 37 40 jaeqifi 
 |-  ( if ( z R y , <. z , y >. , <. y , z >. ) = if ( w R y , <. w , y >. , <. y , w >. ) -> ( -. y = w -> z = w ) )
42 28 41 syl5com 
 |-  ( w e. ( A \ { y } ) -> ( if ( z R y , <. z , y >. , <. y , z >. ) = if ( w R y , <. w , y >. , <. y , w >. ) -> z = w ) )
43 42 rgen 
 |-  A. w e. ( A \ { y } ) ( if ( z R y , <. z , y >. , <. y , z >. ) = if ( w R y , <. w , y >. , <. y , w >. ) -> z = w )
44 43 rgenw 
 |-  A. z e. ( A \ { y } ) A. w e. ( A \ { y } ) ( if ( z R y , <. z , y >. , <. y , z >. ) = if ( w R y , <. w , y >. , <. y , w >. ) -> z = w )
45 eqid 
 |-  ( z e. ( A \ { y } ) |-> if ( z R y , <. z , y >. , <. y , z >. ) ) = ( z e. ( A \ { y } ) |-> if ( z R y , <. z , y >. , <. y , z >. ) )
46 breq1 
 |-  ( z = w -> ( z R y <-> w R y ) )
47 opeq1 
 |-  ( z = w -> <. z , y >. = <. w , y >. )
48 opeq2 
 |-  ( z = w -> <. y , z >. = <. y , w >. )
49 46 47 48 ifbieq12d 
 |-  ( z = w -> if ( z R y , <. z , y >. , <. y , z >. ) = if ( w R y , <. w , y >. , <. y , w >. ) )
50 45 49 f1mpt 
 |-  ( ( z e. ( A \ { y } ) |-> if ( z R y , <. z , y >. , <. y , z >. ) ) : ( A \ { y } ) -1-1-> R <-> ( A. z e. ( A \ { y } ) if ( z R y , <. z , y >. , <. y , z >. ) e. R /\ A. z e. ( A \ { y } ) A. w e. ( A \ { y } ) ( if ( z R y , <. z , y >. , <. y , z >. ) = if ( w R y , <. w , y >. , <. y , w >. ) -> z = w ) ) )
51 26 44 50 sylanblrc 
 |-  ( ( R Or A /\ y e. A ) -> ( z e. ( A \ { y } ) |-> if ( z R y , <. z , y >. , <. y , z >. ) ) : ( A \ { y } ) -1-1-> R )
52 f1domg 
 |-  ( R e. V -> ( ( z e. ( A \ { y } ) |-> if ( z R y , <. z , y >. , <. y , z >. ) ) : ( A \ { y } ) -1-1-> R -> ( A \ { y } ) ~<_ R ) )
53 51 52 syl5 
 |-  ( R e. V -> ( ( R Or A /\ y e. A ) -> ( A \ { y } ) ~<_ R ) )
54 53 impl 
 |-  ( ( ( R e. V /\ R Or A ) /\ y e. A ) -> ( A \ { y } ) ~<_ R )
55 endomtr 
 |-  ( ( A ~~ ( A \ { y } ) /\ ( A \ { y } ) ~<_ R ) -> A ~<_ R )
56 6 54 55 syl3an132 
 |-  ( ( _om ~<_ A /\ ( R e. V /\ R Or A ) /\ y e. A ) -> A ~<_ R )
57 56 3expia 
 |-  ( ( _om ~<_ A /\ ( R e. V /\ R Or A ) ) -> ( y e. A -> A ~<_ R ) )
58 57 exlimdv 
 |-  ( ( _om ~<_ A /\ ( R e. V /\ R Or A ) ) -> ( E. y y e. A -> A ~<_ R ) )
59 4 58 mpd 
 |-  ( ( _om ~<_ A /\ ( R e. V /\ R Or A ) ) -> A ~<_ R )
60 59 ancom2s 
 |-  ( ( _om ~<_ A /\ ( R Or A /\ R e. V ) ) -> A ~<_ R )
61 60 ancoms 
 |-  ( ( ( R Or A /\ R e. V ) /\ _om ~<_ A ) -> A ~<_ R )
62 61 3impa 
 |-  ( ( R Or A /\ R e. V /\ _om ~<_ A ) -> A ~<_ R )