Theorem rankeq0 4758

Description: A set is empty iff its rank is empty.

Hypothesis

Ref	Expression
rankeq0.1	⊢ A ∈ V

Assertion

Ref	Expression
rankeq0	⊢ (A = ∅ ↔ (rank ‘A) = ∅)

Proof of Theorem rankeq0

Step	Hyp	Ref	Expression
1		fveq2 3781	. . 3 ⊢ (A = ∅ → (rank ‘A) = (rank ‘∅))
2		0elon 3079	. . . 4 ⊢ ∅ ∈ On
3		rankonid 4757	. . . 4 ⊢ (∅ ∈ On ↔ (rank ‘∅) = ∅)
4	2, 3	mpbi 196	. . 3 ⊢ (rank ‘∅) = ∅
5	1, 4	syl6eq 1570	. 2 ⊢ (A = ∅ → (rank ‘A) = ∅)
6		rankeq0.1	. . . . 5 ⊢ A ∈ V
7		rankval2 4732	. . . . 5 ⊢ (A ∈ V → (rank ‘A) = ∩{x ∈ On∣A ⊆ (R1 ‘x)})
8	6, 7	ax-mp 7	. . . 4 ⊢ (rank ‘A) = ∩{x ∈ On∣A ⊆ (R1 ‘x)}
9	8	eqeq1i 1529	. . 3 ⊢ ((rank ‘A) = ∅ ↔ ∩{x ∈ On∣A ⊆ (R1 ‘x)} = ∅)
10		ssrab2 2182	. . . . . 6 ⊢ {x ∈ On∣A ⊆ (R1 ‘x)} ⊆ On
11		onint0 3064	. . . . . 6 ⊢ ({x ∈ On∣A ⊆ (R1 ‘x)} ⊆ On → (∩{x ∈ On∣A ⊆ (R1 ‘x)} = ∅ ↔ ∅ ∈ {x ∈ On∣A ⊆ (R1 ‘x)}))
12	10, 11	ax-mp 7	. . . . 5 ⊢ (∩{x ∈ On∣A ⊆ (R1 ‘x)} = ∅ ↔ ∅ ∈ {x ∈ On∣A ⊆ (R1 ‘x)})
13		fveq2 3781	. . . . . . 7 ⊢ (x = ∅ → (R1 ‘x) = (R1 ‘∅))
14	13	sseq2d 2140	. . . . . 6 ⊢ (x = ∅ → (A ⊆ (R1 ‘x) ↔ A ⊆ (R1 ‘∅)))
15	14	elrab 1952	. . . . 5 ⊢ (∅ ∈ {x ∈ On∣A ⊆ (R1 ‘x)} ↔ (∅ ∈ On ⋀ A ⊆ (R1 ‘∅)))
16	2	biantrur 737	. . . . . 6 ⊢ (A ⊆ (R1 ‘∅) ↔ (∅ ∈ On ⋀ A ⊆ (R1 ‘∅)))
17		r10 4713	. . . . . . 7 ⊢ (R1 ‘∅) = ∅
18	17	sseq2i 2137	. . . . . 6 ⊢ (A ⊆ (R1 ‘∅) ↔ A ⊆ ∅)
19	16, 18	bitr3i 182	. . . . 5 ⊢ ((∅ ∈ On ⋀ A ⊆ (R1 ‘∅)) ↔ A ⊆ ∅)
20	12, 15, 19	3bitri 184	. . . 4 ⊢ (∩{x ∈ On∣A ⊆ (R1 ‘x)} = ∅ ↔ A ⊆ ∅)
21		ss0 2355	. . . 4 ⊢ (A ⊆ ∅ → A = ∅)
22	20, 21	sylbi 206	. . 3 ⊢ (∩{x ∈ On∣A ⊆ (R1 ‘x)} = ∅ → A = ∅)
23	9, 22	sylbi 206	. 2 ⊢ ((rank ‘A) = ∅ → A = ∅)
24	5, 23	impbii 164	1 ⊢ (A = ∅ ↔ (rank ‘A) = ∅)

Syntax hints:   ↔ wb 153   ⋀ wa 230   = wceq 997   ∈ wcel 999  {crab 1695  Vcvv 1858   ⊆ wss 2098  ∅c0 2331  ∩cint 2587  Oncon0 3005   ‘cfv 3239  R₁cr1 4703  rankcrnk 4704

This theorem is referenced by:  rankxplim2 4775  rankxplim3 4776  rankxpsuc 4777

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1003  ax-gen 1004  ax-8 1005  ax-9 1006  ax-10 1007  ax-11 1008  ax-12 1009  ax-13 1010  ax-14 1011  ax-17 1012  ax-4 1014  ax-5o 1016  ax-6o 1019  ax-9o 1164  ax-10o 1182  ax-16 1252  ax-11o 1260  ax-ext 1504  ax-rep 2748  ax-sep 2758  ax-nul 2765  ax-pow 2798  ax-pr 2835  ax-un 2922  ax-reg 4653  ax-inf2 4687

This theorem depends on definitions:  df-bi 154  df-or 231  df-an 232  df-3or 788  df-3an 789  df-ex 1022  df-sb 1214  df-eu 1424  df-mo 1425  df-clab 1510  df-cleq 1515  df-clel 1518  df-ne 1634  df-ral 1696  df-rex 1697  df-rab 1699  df-v 1859  df-sbc 1989  df-dif 2100  df-un 2101  df-in 2102  df-ss 2104  df-nul 2332  df-if 2414  df-pw 2454  df-sn 2464  df-pr 2465  df-tp 2467  df-op 2468  df-uni 2558  df-int 2588  df-iun 2622  df-br 2675  df-opab 2722  df-tr 2736  df-eprel 2888  df-id 2891  df-po 2896  df-so 2906  df-fr 2974  df-we 2991  df-ord 3008  df-on 3009  df-lim 3010  df-suc 3011  df-om 3189  df-xp 3241  df-rel 3242  df-cnv 3243  df-co 3244  df-dm 3245  df-rn 3246  df-res 3247  df-ima 3248  df-fun 3249  df-fn 3250  df-fv 3255  df-rdg 3990  df-r1 4705  df-rank 4706

Copyright terms: Public domain