Theorem 1sdom

Description: A set that strictly dominates ordinal 1 has at least 2 different members. (Closely related to 2dom .) (Contributed by Mario Carneiro, 12-Jan-2013)

	Ref	Expression
Assertion	1sdom	⊢ ( 𝐴 ∈ 𝑉 → ( 1o ≺ 𝐴 ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ¬ 𝑥 = 𝑦 ) )

Proof

Step	Hyp	Ref	Expression
1		breq2	⊢ ( 𝑎 = 𝐴 → ( 1o ≺ 𝑎 ↔ 1o ≺ 𝐴 ) )
2		rexeq	⊢ ( 𝑎 = 𝐴 → ( ∃ 𝑦 ∈ 𝑎 ¬ 𝑥 = 𝑦 ↔ ∃ 𝑦 ∈ 𝐴 ¬ 𝑥 = 𝑦 ) )
3	2	rexeqbi1dv	⊢ ( 𝑎 = 𝐴 → ( ∃ 𝑥 ∈ 𝑎 ∃ 𝑦 ∈ 𝑎 ¬ 𝑥 = 𝑦 ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ¬ 𝑥 = 𝑦 ) )
4		1onn	⊢ 1o ∈ ω
5		sucdom	⊢ ( 1o ∈ ω → ( 1o ≺ 𝑎 ↔ suc 1o ≼ 𝑎 ) )
6	4 5	ax-mp	⊢ ( 1o ≺ 𝑎 ↔ suc 1o ≼ 𝑎 )
7		df-2o	⊢ 2o = suc 1o
8	7	breq1i	⊢ ( 2o ≼ 𝑎 ↔ suc 1o ≼ 𝑎 )
9		2dom	⊢ ( 2o ≼ 𝑎 → ∃ 𝑥 ∈ 𝑎 ∃ 𝑦 ∈ 𝑎 ¬ 𝑥 = 𝑦 )
10		df2o3	⊢ 2o = { ∅ , 1o }
11		vex	⊢ 𝑥 ∈ V
12		vex	⊢ 𝑦 ∈ V
13		0ex	⊢ ∅ ∈ V
14		1oex	⊢ 1o ∈ V
15	11 12 13 14	funpr	⊢ ( 𝑥 ≠ 𝑦 → Fun { ⟨ 𝑥 , ∅ ⟩ , ⟨ 𝑦 , 1o ⟩ } )
16		df-ne	⊢ ( 𝑥 ≠ 𝑦 ↔ ¬ 𝑥 = 𝑦 )
17		1n0	⊢ 1o ≠ ∅
18	17	necomi	⊢ ∅ ≠ 1o
19	13 14 11 12	fpr	⊢ ( ∅ ≠ 1o → { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } : { ∅ , 1o } ⟶ { 𝑥 , 𝑦 } )
20	18 19	ax-mp	⊢ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } : { ∅ , 1o } ⟶ { 𝑥 , 𝑦 }
21		df-f1	⊢ ( { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } : { ∅ , 1o } –1-1→ { 𝑥 , 𝑦 } ↔ ( { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } : { ∅ , 1o } ⟶ { 𝑥 , 𝑦 } ∧ Fun ◡ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ) )
22	20 21	mpbiran	⊢ ( { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } : { ∅ , 1o } –1-1→ { 𝑥 , 𝑦 } ↔ Fun ◡ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } )
23	13 11	cnvsn	⊢ ◡ { ⟨ ∅ , 𝑥 ⟩ } = { ⟨ 𝑥 , ∅ ⟩ }
24	14 12	cnvsn	⊢ ◡ { ⟨ 1o , 𝑦 ⟩ } = { ⟨ 𝑦 , 1o ⟩ }
25	23 24	uneq12i	⊢ ( ◡ { ⟨ ∅ , 𝑥 ⟩ } ∪ ◡ { ⟨ 1o , 𝑦 ⟩ } ) = ( { ⟨ 𝑥 , ∅ ⟩ } ∪ { ⟨ 𝑦 , 1o ⟩ } )
26		df-pr	⊢ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } = ( { ⟨ ∅ , 𝑥 ⟩ } ∪ { ⟨ 1o , 𝑦 ⟩ } )
27	26	cnveqi	⊢ ◡ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } = ◡ ( { ⟨ ∅ , 𝑥 ⟩ } ∪ { ⟨ 1o , 𝑦 ⟩ } )
28		cnvun	⊢ ◡ ( { ⟨ ∅ , 𝑥 ⟩ } ∪ { ⟨ 1o , 𝑦 ⟩ } ) = ( ◡ { ⟨ ∅ , 𝑥 ⟩ } ∪ ◡ { ⟨ 1o , 𝑦 ⟩ } )
29	27 28	eqtri	⊢ ◡ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } = ( ◡ { ⟨ ∅ , 𝑥 ⟩ } ∪ ◡ { ⟨ 1o , 𝑦 ⟩ } )
30		df-pr	⊢ { ⟨ 𝑥 , ∅ ⟩ , ⟨ 𝑦 , 1o ⟩ } = ( { ⟨ 𝑥 , ∅ ⟩ } ∪ { ⟨ 𝑦 , 1o ⟩ } )
31	25 29 30	3eqtr4i	⊢ ◡ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } = { ⟨ 𝑥 , ∅ ⟩ , ⟨ 𝑦 , 1o ⟩ }
32	31	funeqi	⊢ ( Fun ◡ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ↔ Fun { ⟨ 𝑥 , ∅ ⟩ , ⟨ 𝑦 , 1o ⟩ } )
33	22 32	bitr2i	⊢ ( Fun { ⟨ 𝑥 , ∅ ⟩ , ⟨ 𝑦 , 1o ⟩ } ↔ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } : { ∅ , 1o } –1-1→ { 𝑥 , 𝑦 } )
34	15 16 33	3imtr3i	⊢ ( ¬ 𝑥 = 𝑦 → { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } : { ∅ , 1o } –1-1→ { 𝑥 , 𝑦 } )
35		prssi	⊢ ( ( 𝑥 ∈ 𝑎 ∧ 𝑦 ∈ 𝑎 ) → { 𝑥 , 𝑦 } ⊆ 𝑎 )
36		f1ss	⊢ ( ( { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } : { ∅ , 1o } –1-1→ { 𝑥 , 𝑦 } ∧ { 𝑥 , 𝑦 } ⊆ 𝑎 ) → { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } : { ∅ , 1o } –1-1→ 𝑎 )
37	34 35 36	syl2an	⊢ ( ( ¬ 𝑥 = 𝑦 ∧ ( 𝑥 ∈ 𝑎 ∧ 𝑦 ∈ 𝑎 ) ) → { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } : { ∅ , 1o } –1-1→ 𝑎 )
38		prex	⊢ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } ∈ V
39		f1eq1	⊢ ( 𝑓 = { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } → ( 𝑓 : { ∅ , 1o } –1-1→ 𝑎 ↔ { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } : { ∅ , 1o } –1-1→ 𝑎 ) )
40	38 39	spcev	⊢ ( { ⟨ ∅ , 𝑥 ⟩ , ⟨ 1o , 𝑦 ⟩ } : { ∅ , 1o } –1-1→ 𝑎 → ∃ 𝑓 𝑓 : { ∅ , 1o } –1-1→ 𝑎 )
41	37 40	syl	⊢ ( ( ¬ 𝑥 = 𝑦 ∧ ( 𝑥 ∈ 𝑎 ∧ 𝑦 ∈ 𝑎 ) ) → ∃ 𝑓 𝑓 : { ∅ , 1o } –1-1→ 𝑎 )
42		vex	⊢ 𝑎 ∈ V
43	42	brdom	⊢ ( { ∅ , 1o } ≼ 𝑎 ↔ ∃ 𝑓 𝑓 : { ∅ , 1o } –1-1→ 𝑎 )
44	41 43	sylibr	⊢ ( ( ¬ 𝑥 = 𝑦 ∧ ( 𝑥 ∈ 𝑎 ∧ 𝑦 ∈ 𝑎 ) ) → { ∅ , 1o } ≼ 𝑎 )
45	44	expcom	⊢ ( ( 𝑥 ∈ 𝑎 ∧ 𝑦 ∈ 𝑎 ) → ( ¬ 𝑥 = 𝑦 → { ∅ , 1o } ≼ 𝑎 ) )
46	45	rexlimivv	⊢ ( ∃ 𝑥 ∈ 𝑎 ∃ 𝑦 ∈ 𝑎 ¬ 𝑥 = 𝑦 → { ∅ , 1o } ≼ 𝑎 )
47	10 46	eqbrtrid	⊢ ( ∃ 𝑥 ∈ 𝑎 ∃ 𝑦 ∈ 𝑎 ¬ 𝑥 = 𝑦 → 2o ≼ 𝑎 )
48	9 47	impbii	⊢ ( 2o ≼ 𝑎 ↔ ∃ 𝑥 ∈ 𝑎 ∃ 𝑦 ∈ 𝑎 ¬ 𝑥 = 𝑦 )
49	6 8 48	3bitr2i	⊢ ( 1o ≺ 𝑎 ↔ ∃ 𝑥 ∈ 𝑎 ∃ 𝑦 ∈ 𝑎 ¬ 𝑥 = 𝑦 )
50	1 3 49	vtoclbg	⊢ ( 𝐴 ∈ 𝑉 → ( 1o ≺ 𝐴 ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ¬ 𝑥 = 𝑦 ) )