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 ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑥 ≼ 𝑦 ∨ 𝑦 ≼ 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		dfac10c	⊢ ( CHOICE ↔ ∀ 𝑥 ∃ 𝑤 ∈ On 𝑤 ≈ 𝑥 )
2		dfac10c	⊢ ( CHOICE ↔ ∀ 𝑦 ∃ 𝑧 ∈ On 𝑧 ≈ 𝑦 )
3		domtriord	⊢ ( ( 𝑤 ∈ On ∧ 𝑧 ∈ On ) → ( 𝑤 ≼ 𝑧 ↔ ¬ 𝑧 ≺ 𝑤 ) )
4		xor3	⊢ ( ¬ ( 𝑤 ≼ 𝑧 ↔ 𝑧 ≺ 𝑤 ) ↔ ( 𝑤 ≼ 𝑧 ↔ ¬ 𝑧 ≺ 𝑤 ) )
5		nbior	⊢ ( ¬ ( 𝑤 ≼ 𝑧 ↔ 𝑧 ≺ 𝑤 ) → ( 𝑤 ≼ 𝑧 ∨ 𝑧 ≺ 𝑤 ) )
6	4 5	sylbir	⊢ ( ( 𝑤 ≼ 𝑧 ↔ ¬ 𝑧 ≺ 𝑤 ) → ( 𝑤 ≼ 𝑧 ∨ 𝑧 ≺ 𝑤 ) )
7	3 6	syl	⊢ ( ( 𝑤 ∈ On ∧ 𝑧 ∈ On ) → ( 𝑤 ≼ 𝑧 ∨ 𝑧 ≺ 𝑤 ) )
8		ensym	⊢ ( 𝑤 ≈ 𝑥 → 𝑥 ≈ 𝑤 )
9		endomtr	⊢ ( ( 𝑥 ≈ 𝑤 ∧ 𝑤 ≼ 𝑧 ) → 𝑥 ≼ 𝑧 )
10	8 9	sylan	⊢ ( ( 𝑤 ≈ 𝑥 ∧ 𝑤 ≼ 𝑧 ) → 𝑥 ≼ 𝑧 )
11	10	ex	⊢ ( 𝑤 ≈ 𝑥 → ( 𝑤 ≼ 𝑧 → 𝑥 ≼ 𝑧 ) )
12		domentr	⊢ ( ( 𝑥 ≼ 𝑧 ∧ 𝑧 ≈ 𝑦 ) → 𝑥 ≼ 𝑦 )
13	12	expcom	⊢ ( 𝑧 ≈ 𝑦 → ( 𝑥 ≼ 𝑧 → 𝑥 ≼ 𝑦 ) )
14	11 13	sylan9	⊢ ( ( 𝑤 ≈ 𝑥 ∧ 𝑧 ≈ 𝑦 ) → ( 𝑤 ≼ 𝑧 → 𝑥 ≼ 𝑦 ) )
15		ensym	⊢ ( 𝑧 ≈ 𝑦 → 𝑦 ≈ 𝑧 )
16		sdomdom	⊢ ( 𝑧 ≺ 𝑤 → 𝑧 ≼ 𝑤 )
17		endomtr	⊢ ( ( 𝑦 ≈ 𝑧 ∧ 𝑧 ≼ 𝑤 ) → 𝑦 ≼ 𝑤 )
18	15 16 17	syl2an	⊢ ( ( 𝑧 ≈ 𝑦 ∧ 𝑧 ≺ 𝑤 ) → 𝑦 ≼ 𝑤 )
19	18	ex	⊢ ( 𝑧 ≈ 𝑦 → ( 𝑧 ≺ 𝑤 → 𝑦 ≼ 𝑤 ) )
20		domentr	⊢ ( ( 𝑦 ≼ 𝑤 ∧ 𝑤 ≈ 𝑥 ) → 𝑦 ≼ 𝑥 )
21	20	expcom	⊢ ( 𝑤 ≈ 𝑥 → ( 𝑦 ≼ 𝑤 → 𝑦 ≼ 𝑥 ) )
22	19 21	sylan9r	⊢ ( ( 𝑤 ≈ 𝑥 ∧ 𝑧 ≈ 𝑦 ) → ( 𝑧 ≺ 𝑤 → 𝑦 ≼ 𝑥 ) )
23	14 22	orim12d	⊢ ( ( 𝑤 ≈ 𝑥 ∧ 𝑧 ≈ 𝑦 ) → ( ( 𝑤 ≼ 𝑧 ∨ 𝑧 ≺ 𝑤 ) → ( 𝑥 ≼ 𝑦 ∨ 𝑦 ≼ 𝑥 ) ) )
24	7 23	mpan9	⊢ ( ( ( 𝑤 ∈ On ∧ 𝑧 ∈ On ) ∧ ( 𝑤 ≈ 𝑥 ∧ 𝑧 ≈ 𝑦 ) ) → ( 𝑥 ≼ 𝑦 ∨ 𝑦 ≼ 𝑥 ) )
25	24	an4s	⊢ ( ( ( 𝑤 ∈ On ∧ 𝑤 ≈ 𝑥 ) ∧ ( 𝑧 ∈ On ∧ 𝑧 ≈ 𝑦 ) ) → ( 𝑥 ≼ 𝑦 ∨ 𝑦 ≼ 𝑥 ) )
26	25	rexlimdvaa	⊢ ( ( 𝑤 ∈ On ∧ 𝑤 ≈ 𝑥 ) → ( ∃ 𝑧 ∈ On 𝑧 ≈ 𝑦 → ( 𝑥 ≼ 𝑦 ∨ 𝑦 ≼ 𝑥 ) ) )
27	26	alimdv	⊢ ( ( 𝑤 ∈ On ∧ 𝑤 ≈ 𝑥 ) → ( ∀ 𝑦 ∃ 𝑧 ∈ On 𝑧 ≈ 𝑦 → ∀ 𝑦 ( 𝑥 ≼ 𝑦 ∨ 𝑦 ≼ 𝑥 ) ) )
28	2 27	biimtrid	⊢ ( ( 𝑤 ∈ On ∧ 𝑤 ≈ 𝑥 ) → ( CHOICE → ∀ 𝑦 ( 𝑥 ≼ 𝑦 ∨ 𝑦 ≼ 𝑥 ) ) )
29	28	rexlimiva	⊢ ( ∃ 𝑤 ∈ On 𝑤 ≈ 𝑥 → ( CHOICE → ∀ 𝑦 ( 𝑥 ≼ 𝑦 ∨ 𝑦 ≼ 𝑥 ) ) )
30	29	com12	⊢ ( CHOICE → ( ∃ 𝑤 ∈ On 𝑤 ≈ 𝑥 → ∀ 𝑦 ( 𝑥 ≼ 𝑦 ∨ 𝑦 ≼ 𝑥 ) ) )
31	30	alimdv	⊢ ( CHOICE → ( ∀ 𝑥 ∃ 𝑤 ∈ On 𝑤 ≈ 𝑥 → ∀ 𝑥 ∀ 𝑦 ( 𝑥 ≼ 𝑦 ∨ 𝑦 ≼ 𝑥 ) ) )
32	1 31	biimtrid	⊢ ( CHOICE → ( CHOICE → ∀ 𝑥 ∀ 𝑦 ( 𝑥 ≼ 𝑦 ∨ 𝑦 ≼ 𝑥 ) ) )
33	32	pm2.43i	⊢ ( CHOICE → ∀ 𝑥 ∀ 𝑦 ( 𝑥 ≼ 𝑦 ∨ 𝑦 ≼ 𝑥 ) )
34		breq2	⊢ ( 𝑣 = ( har ‘ 𝑥 ) → ( 𝑥 ≼ 𝑣 ↔ 𝑥 ≼ ( har ‘ 𝑥 ) ) )
35		harcl	⊢ ( har ‘ 𝑥 ) ∈ On
36	35	a1i	⊢ ( ∀ 𝑦 ( 𝑥 ≼ 𝑦 ∨ 𝑦 ≼ 𝑥 ) → ( har ‘ 𝑥 ) ∈ On )
37		fvex	⊢ ( har ‘ 𝑥 ) ∈ V
38		breq2	⊢ ( 𝑦 = ( har ‘ 𝑥 ) → ( 𝑥 ≼ 𝑦 ↔ 𝑥 ≼ ( har ‘ 𝑥 ) ) )
39		breq1	⊢ ( 𝑦 = ( har ‘ 𝑥 ) → ( 𝑦 ≼ 𝑥 ↔ ( har ‘ 𝑥 ) ≼ 𝑥 ) )
40	38 39	orbi12d	⊢ ( 𝑦 = ( har ‘ 𝑥 ) → ( ( 𝑥 ≼ 𝑦 ∨ 𝑦 ≼ 𝑥 ) ↔ ( 𝑥 ≼ ( har ‘ 𝑥 ) ∨ ( har ‘ 𝑥 ) ≼ 𝑥 ) ) )
41	37 40	spcv	⊢ ( ∀ 𝑦 ( 𝑥 ≼ 𝑦 ∨ 𝑦 ≼ 𝑥 ) → ( 𝑥 ≼ ( har ‘ 𝑥 ) ∨ ( har ‘ 𝑥 ) ≼ 𝑥 ) )
42		harndom	⊢ ¬ ( har ‘ 𝑥 ) ≼ 𝑥
43	42	a1i	⊢ ( ∀ 𝑦 ( 𝑥 ≼ 𝑦 ∨ 𝑦 ≼ 𝑥 ) → ¬ ( har ‘ 𝑥 ) ≼ 𝑥 )
44	41 43	olcnd	⊢ ( ∀ 𝑦 ( 𝑥 ≼ 𝑦 ∨ 𝑦 ≼ 𝑥 ) → 𝑥 ≼ ( har ‘ 𝑥 ) )
45	34 36 44	rspcedvdw	⊢ ( ∀ 𝑦 ( 𝑥 ≼ 𝑦 ∨ 𝑦 ≼ 𝑥 ) → ∃ 𝑣 ∈ On 𝑥 ≼ 𝑣 )
46		ac10ct	⊢ ( ∃ 𝑣 ∈ On 𝑥 ≼ 𝑣 → ∃ 𝑟 𝑟 We 𝑥 )
47	45 46	syl	⊢ ( ∀ 𝑦 ( 𝑥 ≼ 𝑦 ∨ 𝑦 ≼ 𝑥 ) → ∃ 𝑟 𝑟 We 𝑥 )
48	47	alimi	⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 ≼ 𝑦 ∨ 𝑦 ≼ 𝑥 ) → ∀ 𝑥 ∃ 𝑟 𝑟 We 𝑥 )
49		dfac8	⊢ ( CHOICE ↔ ∀ 𝑥 ∃ 𝑟 𝑟 We 𝑥 )
50	48 49	sylibr	⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 ≼ 𝑦 ∨ 𝑦 ≼ 𝑥 ) → CHOICE )
51	33 50	impbii	⊢ ( CHOICE ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑥 ≼ 𝑦 ∨ 𝑦 ≼ 𝑥 ) )