Metamath Proof Explorer

Theorem dfac16

Description: Axiom of Choice equivalent: for every pair of sets, one is dominated by the other (see also entri3 ). (Contributed by BTernaryTau, 17-Sep-2026)

Ref Expression
Assertion dfac16 
|- ( CHOICE <-> A. x A. y ( x ~<_ y \/ y ~<_ x ) )

Proof

Step Hyp Ref Expression
1 dfac10c 
 |-  ( CHOICE <-> A. x E. w e. On w ~~ x )
2 dfac10c 
 |-  ( CHOICE <-> A. y E. z e. On z ~~ y )
3 domtriord 
 |-  ( ( w e. On /\ z e. On ) -> ( w ~<_ z <-> -. z ~< w ) )
4 xor3 
 |-  ( -. ( w ~<_ z <-> z ~< w ) <-> ( w ~<_ z <-> -. z ~< w ) )
5 nbior 
 |-  ( -. ( w ~<_ z <-> z ~< w ) -> ( w ~<_ z \/ z ~< w ) )
6 4 5 sylbir 
 |-  ( ( w ~<_ z <-> -. z ~< w ) -> ( w ~<_ z \/ z ~< w ) )
7 3 6 syl 
 |-  ( ( w e. On /\ z e. On ) -> ( w ~<_ z \/ z ~< w ) )
8 ensym 
 |-  ( w ~~ x -> x ~~ w )
9 endomtr 
 |-  ( ( x ~~ w /\ w ~<_ z ) -> x ~<_ z )
10 8 9 sylan 
 |-  ( ( w ~~ x /\ w ~<_ z ) -> x ~<_ z )
11 10 ex 
 |-  ( w ~~ x -> ( w ~<_ z -> x ~<_ z ) )
12 domentr 
 |-  ( ( x ~<_ z /\ z ~~ y ) -> x ~<_ y )
13 12 expcom 
 |-  ( z ~~ y -> ( x ~<_ z -> x ~<_ y ) )
14 11 13 sylan9 
 |-  ( ( w ~~ x /\ z ~~ y ) -> ( w ~<_ z -> x ~<_ y ) )
15 ensym 
 |-  ( z ~~ y -> y ~~ z )
16 sdomdom 
 |-  ( z ~< w -> z ~<_ w )
17 endomtr 
 |-  ( ( y ~~ z /\ z ~<_ w ) -> y ~<_ w )
18 15 16 17 syl2an 
 |-  ( ( z ~~ y /\ z ~< w ) -> y ~<_ w )
19 18 ex 
 |-  ( z ~~ y -> ( z ~< w -> y ~<_ w ) )
20 domentr 
 |-  ( ( y ~<_ w /\ w ~~ x ) -> y ~<_ x )
21 20 expcom 
 |-  ( w ~~ x -> ( y ~<_ w -> y ~<_ x ) )
22 19 21 sylan9r 
 |-  ( ( w ~~ x /\ z ~~ y ) -> ( z ~< w -> y ~<_ x ) )
23 14 22 orim12d 
 |-  ( ( w ~~ x /\ z ~~ y ) -> ( ( w ~<_ z \/ z ~< w ) -> ( x ~<_ y \/ y ~<_ x ) ) )
24 7 23 mpan9 
 |-  ( ( ( w e. On /\ z e. On ) /\ ( w ~~ x /\ z ~~ y ) ) -> ( x ~<_ y \/ y ~<_ x ) )
25 24 an4s 
 |-  ( ( ( w e. On /\ w ~~ x ) /\ ( z e. On /\ z ~~ y ) ) -> ( x ~<_ y \/ y ~<_ x ) )
26 25 rexlimdvaa 
 |-  ( ( w e. On /\ w ~~ x ) -> ( E. z e. On z ~~ y -> ( x ~<_ y \/ y ~<_ x ) ) )
27 26 alimdv 
 |-  ( ( w e. On /\ w ~~ x ) -> ( A. y E. z e. On z ~~ y -> A. y ( x ~<_ y \/ y ~<_ x ) ) )
28 2 27 biimtrid 
 |-  ( ( w e. On /\ w ~~ x ) -> ( CHOICE -> A. y ( x ~<_ y \/ y ~<_ x ) ) )
29 28 rexlimiva 
 |-  ( E. w e. On w ~~ x -> ( CHOICE -> A. y ( x ~<_ y \/ y ~<_ x ) ) )
30 29 com12 
 |-  ( CHOICE -> ( E. w e. On w ~~ x -> A. y ( x ~<_ y \/ y ~<_ x ) ) )
31 30 alimdv 
 |-  ( CHOICE -> ( A. x E. w e. On w ~~ x -> A. x A. y ( x ~<_ y \/ y ~<_ x ) ) )
32 1 31 biimtrid 
 |-  ( CHOICE -> ( CHOICE -> A. x A. y ( x ~<_ y \/ y ~<_ x ) ) )
33 32 pm2.43i 
 |-  ( CHOICE -> A. x A. y ( x ~<_ y \/ y ~<_ x ) )
34 breq2 
 |-  ( v = ( har ` x ) -> ( x ~<_ v <-> x ~<_ ( har ` x ) ) )
35 harcl 
 |-  ( har ` x ) e. On
36 35 a1i 
 |-  ( A. y ( x ~<_ y \/ y ~<_ x ) -> ( har ` x ) e. On )
37 fvex 
 |-  ( har ` x ) e. _V
38 breq2 
 |-  ( y = ( har ` x ) -> ( x ~<_ y <-> x ~<_ ( har ` x ) ) )
39 breq1 
 |-  ( y = ( har ` x ) -> ( y ~<_ x <-> ( har ` x ) ~<_ x ) )
40 38 39 orbi12d 
 |-  ( y = ( har ` x ) -> ( ( x ~<_ y \/ y ~<_ x ) <-> ( x ~<_ ( har ` x ) \/ ( har ` x ) ~<_ x ) ) )
41 37 40 spcv 
 |-  ( A. y ( x ~<_ y \/ y ~<_ x ) -> ( x ~<_ ( har ` x ) \/ ( har ` x ) ~<_ x ) )
42 harndom 
 |-  -. ( har ` x ) ~<_ x
43 42 a1i 
 |-  ( A. y ( x ~<_ y \/ y ~<_ x ) -> -. ( har ` x ) ~<_ x )
44 41 43 olcnd 
 |-  ( A. y ( x ~<_ y \/ y ~<_ x ) -> x ~<_ ( har ` x ) )
45 34 36 44 rspcedvdw 
 |-  ( A. y ( x ~<_ y \/ y ~<_ x ) -> E. v e. On x ~<_ v )
46 ac10ct 
 |-  ( E. v e. On x ~<_ v -> E. r r We x )
47 45 46 syl 
 |-  ( A. y ( x ~<_ y \/ y ~<_ x ) -> E. r r We x )
48 47 alimi 
 |-  ( A. x A. y ( x ~<_ y \/ y ~<_ x ) -> A. x E. r r We x )
49 dfac8 
 |-  ( CHOICE <-> A. x E. r r We x )
50 48 49 sylibr 
 |-  ( A. x A. y ( x ~<_ y \/ y ~<_ x ) -> CHOICE )
51 33 50 impbii 
 |-  ( CHOICE <-> A. x A. y ( x ~<_ y \/ y ~<_ x ) )