Theorem rankeq1o

Description: The only set with rank 1o is the singleton of the empty set. (Contributed by Scott Fenton, 17-Jul-2015)

	Ref	Expression
Assertion	rankeq1o	⊢ ( ( rank ‘ 𝐴 ) = 1o ↔ 𝐴 = { ∅ } )

Proof

Step	Hyp	Ref	Expression
1		1n0	⊢ 1o ≠ ∅
2		neeq1	⊢ ( ( rank ‘ 𝐴 ) = 1o → ( ( rank ‘ 𝐴 ) ≠ ∅ ↔ 1o ≠ ∅ ) )
3	1 2	mpbiri	⊢ ( ( rank ‘ 𝐴 ) = 1o → ( rank ‘ 𝐴 ) ≠ ∅ )
4	3	neneqd	⊢ ( ( rank ‘ 𝐴 ) = 1o → ¬ ( rank ‘ 𝐴 ) = ∅ )
5		fvprc	⊢ ( ¬ 𝐴 ∈ V → ( rank ‘ 𝐴 ) = ∅ )
6	4 5	nsyl2	⊢ ( ( rank ‘ 𝐴 ) = 1o → 𝐴 ∈ V )
7		fveqeq2	⊢ ( 𝑥 = 𝐴 → ( ( rank ‘ 𝑥 ) = 1o ↔ ( rank ‘ 𝐴 ) = 1o ) )
8		eqeq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 = 1o ↔ 𝐴 = 1o ) )
9	7 8	imbi12d	⊢ ( 𝑥 = 𝐴 → ( ( ( rank ‘ 𝑥 ) = 1o → 𝑥 = 1o ) ↔ ( ( rank ‘ 𝐴 ) = 1o → 𝐴 = 1o ) ) )
10		neeq1	⊢ ( ( rank ‘ 𝑥 ) = 1o → ( ( rank ‘ 𝑥 ) ≠ ∅ ↔ 1o ≠ ∅ ) )
11	1 10	mpbiri	⊢ ( ( rank ‘ 𝑥 ) = 1o → ( rank ‘ 𝑥 ) ≠ ∅ )
12		vex	⊢ 𝑥 ∈ V
13	12	rankeq0	⊢ ( 𝑥 = ∅ ↔ ( rank ‘ 𝑥 ) = ∅ )
14	13	necon3bii	⊢ ( 𝑥 ≠ ∅ ↔ ( rank ‘ 𝑥 ) ≠ ∅ )
15	11 14	sylibr	⊢ ( ( rank ‘ 𝑥 ) = 1o → 𝑥 ≠ ∅ )
16	12	rankval	⊢ ( rank ‘ 𝑥 ) = ∩ { 𝑦 ∈ On ∣ 𝑥 ∈ ( 𝑅1 ‘ suc 𝑦 ) }
17	16	eqeq1i	⊢ ( ( rank ‘ 𝑥 ) = 1o ↔ ∩ { 𝑦 ∈ On ∣ 𝑥 ∈ ( 𝑅1 ‘ suc 𝑦 ) } = 1o )
18		ssrab2	⊢ { 𝑦 ∈ On ∣ 𝑥 ∈ ( 𝑅1 ‘ suc 𝑦 ) } ⊆ On
19		elirr	⊢ ¬ 1o ∈ 1o
20		1oex	⊢ 1o ∈ V
21		id	⊢ ( V = 1o → V = 1o )
22	20 21	eleqtrid	⊢ ( V = 1o → 1o ∈ 1o )
23	19 22	mto	⊢ ¬ V = 1o
24		inteq	⊢ ( { 𝑦 ∈ On ∣ 𝑥 ∈ ( 𝑅1 ‘ suc 𝑦 ) } = ∅ → ∩ { 𝑦 ∈ On ∣ 𝑥 ∈ ( 𝑅1 ‘ suc 𝑦 ) } = ∩ ∅ )
25		int0	⊢ ∩ ∅ = V
26	24 25	eqtrdi	⊢ ( { 𝑦 ∈ On ∣ 𝑥 ∈ ( 𝑅1 ‘ suc 𝑦 ) } = ∅ → ∩ { 𝑦 ∈ On ∣ 𝑥 ∈ ( 𝑅1 ‘ suc 𝑦 ) } = V )
27	26	eqeq1d	⊢ ( { 𝑦 ∈ On ∣ 𝑥 ∈ ( 𝑅1 ‘ suc 𝑦 ) } = ∅ → ( ∩ { 𝑦 ∈ On ∣ 𝑥 ∈ ( 𝑅1 ‘ suc 𝑦 ) } = 1o ↔ V = 1o ) )
28	23 27	mtbiri	⊢ ( { 𝑦 ∈ On ∣ 𝑥 ∈ ( 𝑅1 ‘ suc 𝑦 ) } = ∅ → ¬ ∩ { 𝑦 ∈ On ∣ 𝑥 ∈ ( 𝑅1 ‘ suc 𝑦 ) } = 1o )
29	28	necon2ai	⊢ ( ∩ { 𝑦 ∈ On ∣ 𝑥 ∈ ( 𝑅1 ‘ suc 𝑦 ) } = 1o → { 𝑦 ∈ On ∣ 𝑥 ∈ ( 𝑅1 ‘ suc 𝑦 ) } ≠ ∅ )
30		onint	⊢ ( ( { 𝑦 ∈ On ∣ 𝑥 ∈ ( 𝑅1 ‘ suc 𝑦 ) } ⊆ On ∧ { 𝑦 ∈ On ∣ 𝑥 ∈ ( 𝑅1 ‘ suc 𝑦 ) } ≠ ∅ ) → ∩ { 𝑦 ∈ On ∣ 𝑥 ∈ ( 𝑅1 ‘ suc 𝑦 ) } ∈ { 𝑦 ∈ On ∣ 𝑥 ∈ ( 𝑅1 ‘ suc 𝑦 ) } )
31	18 29 30	sylancr	⊢ ( ∩ { 𝑦 ∈ On ∣ 𝑥 ∈ ( 𝑅1 ‘ suc 𝑦 ) } = 1o → ∩ { 𝑦 ∈ On ∣ 𝑥 ∈ ( 𝑅1 ‘ suc 𝑦 ) } ∈ { 𝑦 ∈ On ∣ 𝑥 ∈ ( 𝑅1 ‘ suc 𝑦 ) } )
32		eleq1	⊢ ( ∩ { 𝑦 ∈ On ∣ 𝑥 ∈ ( 𝑅1 ‘ suc 𝑦 ) } = 1o → ( ∩ { 𝑦 ∈ On ∣ 𝑥 ∈ ( 𝑅1 ‘ suc 𝑦 ) } ∈ { 𝑦 ∈ On ∣ 𝑥 ∈ ( 𝑅1 ‘ suc 𝑦 ) } ↔ 1o ∈ { 𝑦 ∈ On ∣ 𝑥 ∈ ( 𝑅1 ‘ suc 𝑦 ) } ) )
33	31 32	mpbid	⊢ ( ∩ { 𝑦 ∈ On ∣ 𝑥 ∈ ( 𝑅1 ‘ suc 𝑦 ) } = 1o → 1o ∈ { 𝑦 ∈ On ∣ 𝑥 ∈ ( 𝑅1 ‘ suc 𝑦 ) } )
34		suceq	⊢ ( 𝑦 = 1o → suc 𝑦 = suc 1o )
35	34	fveq2d	⊢ ( 𝑦 = 1o → ( 𝑅1 ‘ suc 𝑦 ) = ( 𝑅1 ‘ suc 1o ) )
36		df-1o	⊢ 1o = suc ∅
37	36	fveq2i	⊢ ( 𝑅1 ‘ 1o ) = ( 𝑅1 ‘ suc ∅ )
38		0elon	⊢ ∅ ∈ On
39		r1suc	⊢ ( ∅ ∈ On → ( 𝑅1 ‘ suc ∅ ) = 𝒫 ( 𝑅1 ‘ ∅ ) )
40	38 39	ax-mp	⊢ ( 𝑅1 ‘ suc ∅ ) = 𝒫 ( 𝑅1 ‘ ∅ )
41		r10	⊢ ( 𝑅1 ‘ ∅ ) = ∅
42	41	pweqi	⊢ 𝒫 ( 𝑅1 ‘ ∅ ) = 𝒫 ∅
43	37 40 42	3eqtri	⊢ ( 𝑅1 ‘ 1o ) = 𝒫 ∅
44	43	pweqi	⊢ 𝒫 ( 𝑅1 ‘ 1o ) = 𝒫 𝒫 ∅
45		pw0	⊢ 𝒫 ∅ = { ∅ }
46	45	pweqi	⊢ 𝒫 𝒫 ∅ = 𝒫 { ∅ }
47		pwpw0	⊢ 𝒫 { ∅ } = { ∅ , { ∅ } }
48	44 46 47	3eqtrri	⊢ { ∅ , { ∅ } } = 𝒫 ( 𝑅1 ‘ 1o )
49		1on	⊢ 1o ∈ On
50		r1suc	⊢ ( 1o ∈ On → ( 𝑅1 ‘ suc 1o ) = 𝒫 ( 𝑅1 ‘ 1o ) )
51	49 50	ax-mp	⊢ ( 𝑅1 ‘ suc 1o ) = 𝒫 ( 𝑅1 ‘ 1o )
52	48 51	eqtr4i	⊢ { ∅ , { ∅ } } = ( 𝑅1 ‘ suc 1o )
53	35 52	eqtr4di	⊢ ( 𝑦 = 1o → ( 𝑅1 ‘ suc 𝑦 ) = { ∅ , { ∅ } } )
54	53	eleq2d	⊢ ( 𝑦 = 1o → ( 𝑥 ∈ ( 𝑅1 ‘ suc 𝑦 ) ↔ 𝑥 ∈ { ∅ , { ∅ } } ) )
55	54	elrab	⊢ ( 1o ∈ { 𝑦 ∈ On ∣ 𝑥 ∈ ( 𝑅1 ‘ suc 𝑦 ) } ↔ ( 1o ∈ On ∧ 𝑥 ∈ { ∅ , { ∅ } } ) )
56	33 55	sylib	⊢ ( ∩ { 𝑦 ∈ On ∣ 𝑥 ∈ ( 𝑅1 ‘ suc 𝑦 ) } = 1o → ( 1o ∈ On ∧ 𝑥 ∈ { ∅ , { ∅ } } ) )
57	12	elpr	⊢ ( 𝑥 ∈ { ∅ , { ∅ } } ↔ ( 𝑥 = ∅ ∨ 𝑥 = { ∅ } ) )
58		df-ne	⊢ ( 𝑥 ≠ ∅ ↔ ¬ 𝑥 = ∅ )
59		orel1	⊢ ( ¬ 𝑥 = ∅ → ( ( 𝑥 = ∅ ∨ 𝑥 = { ∅ } ) → 𝑥 = { ∅ } ) )
60	58 59	sylbi	⊢ ( 𝑥 ≠ ∅ → ( ( 𝑥 = ∅ ∨ 𝑥 = { ∅ } ) → 𝑥 = { ∅ } ) )
61		df1o2	⊢ 1o = { ∅ }
62		eqeq2	⊢ ( 𝑥 = { ∅ } → ( 1o = 𝑥 ↔ 1o = { ∅ } ) )
63	61 62	mpbiri	⊢ ( 𝑥 = { ∅ } → 1o = 𝑥 )
64	63	eqcomd	⊢ ( 𝑥 = { ∅ } → 𝑥 = 1o )
65	60 64	syl6com	⊢ ( ( 𝑥 = ∅ ∨ 𝑥 = { ∅ } ) → ( 𝑥 ≠ ∅ → 𝑥 = 1o ) )
66	57 65	sylbi	⊢ ( 𝑥 ∈ { ∅ , { ∅ } } → ( 𝑥 ≠ ∅ → 𝑥 = 1o ) )
67	66	adantl	⊢ ( ( 1o ∈ On ∧ 𝑥 ∈ { ∅ , { ∅ } } ) → ( 𝑥 ≠ ∅ → 𝑥 = 1o ) )
68	56 67	syl	⊢ ( ∩ { 𝑦 ∈ On ∣ 𝑥 ∈ ( 𝑅1 ‘ suc 𝑦 ) } = 1o → ( 𝑥 ≠ ∅ → 𝑥 = 1o ) )
69	17 68	sylbi	⊢ ( ( rank ‘ 𝑥 ) = 1o → ( 𝑥 ≠ ∅ → 𝑥 = 1o ) )
70	15 69	mpd	⊢ ( ( rank ‘ 𝑥 ) = 1o → 𝑥 = 1o )
71	9 70	vtoclg	⊢ ( 𝐴 ∈ V → ( ( rank ‘ 𝐴 ) = 1o → 𝐴 = 1o ) )
72	6 71	mpcom	⊢ ( ( rank ‘ 𝐴 ) = 1o → 𝐴 = 1o )
73		fveq2	⊢ ( 𝐴 = 1o → ( rank ‘ 𝐴 ) = ( rank ‘ 1o ) )
74		r111	⊢ 𝑅1 : On –1-1→ V
75		f1dm	⊢ ( 𝑅1 : On –1-1→ V → dom 𝑅1 = On )
76	74 75	ax-mp	⊢ dom 𝑅1 = On
77	49 76	eleqtrri	⊢ 1o ∈ dom 𝑅1
78		rankonid	⊢ ( 1o ∈ dom 𝑅1 ↔ ( rank ‘ 1o ) = 1o )
79	77 78	mpbi	⊢ ( rank ‘ 1o ) = 1o
80	73 79	eqtrdi	⊢ ( 𝐴 = 1o → ( rank ‘ 𝐴 ) = 1o )
81	72 80	impbii	⊢ ( ( rank ‘ 𝐴 ) = 1o ↔ 𝐴 = 1o )
82	61	eqeq2i	⊢ ( 𝐴 = 1o ↔ 𝐴 = { ∅ } )
83	81 82	bitri	⊢ ( ( rank ‘ 𝐴 ) = 1o ↔ 𝐴 = { ∅ } )