rankeq0b

Description: A set is empty iff its rank is empty. (Contributed by Mario Carneiro, 17-Nov-2014)

		Ref	Expression
	Assertion	rankeq0b	$⊢ A \in ⋃ R_{1} [On] \to (A = \emptyset \leftrightarrow rank (A) = \emptyset)$

Proof

Step	Hyp	Ref	Expression
1		fveq2	$⊢ A = \emptyset \to rank (A) = rank (\emptyset)$
2		r1funlim	$⊢ (Fun R_{1} \land Lim dom R_{1})$
3	2	simpri	$⊢ Lim dom R_{1}$
4		limomss	$⊢ Lim dom R_{1} \to ω \subseteq dom R_{1}$
5	3 4	ax-mp	$⊢ ω \subseteq dom R_{1}$
6		peano1	$⊢ \emptyset \in ω$
7	5 6	sselii	$⊢ \emptyset \in dom R_{1}$
8		rankonid	$⊢ \emptyset \in dom R_{1} \leftrightarrow rank (\emptyset) = \emptyset$
9	7 8	mpbi	$⊢ rank (\emptyset) = \emptyset$
10	1 9	syl6eq	$⊢ A = \emptyset \to rank (A) = \emptyset$
11		eqimss	$⊢ rank (A) = \emptyset \to rank (A) \subseteq \emptyset$
12	11	adantl	$⊢ (A \in ⋃ R_{1} [On] \land rank (A) = \emptyset) \to rank (A) \subseteq \emptyset$
13		simpl	$⊢ (A \in ⋃ R_{1} [On] \land rank (A) = \emptyset) \to A \in ⋃ R_{1} [On]$
14		rankr1bg	$⊢ (A \in ⋃ R_{1} [On] \land \emptyset \in dom R_{1}) \to (A \subseteq R_{1} (\emptyset) \leftrightarrow rank (A) \subseteq \emptyset)$
15	13 7 14	sylancl	$⊢ (A \in ⋃ R_{1} [On] \land rank (A) = \emptyset) \to (A \subseteq R_{1} (\emptyset) \leftrightarrow rank (A) \subseteq \emptyset)$
16	12 15	mpbird	$⊢ (A \in ⋃ R_{1} [On] \land rank (A) = \emptyset) \to A \subseteq R_{1} (\emptyset)$
17		r10	$⊢ R_{1} (\emptyset) = \emptyset$
18	16 17	sseqtrdi	$⊢ (A \in ⋃ R_{1} [On] \land rank (A) = \emptyset) \to A \subseteq \emptyset$
19		ss0	$⊢ A \subseteq \emptyset \to A = \emptyset$
20	18 19	syl	$⊢ (A \in ⋃ R_{1} [On] \land rank (A) = \emptyset) \to A = \emptyset$
21	20	ex	$⊢ A \in ⋃ R_{1} [On] \to (rank (A) = \emptyset \to A = \emptyset)$
22	10 21	impbid2	$⊢ A \in ⋃ R_{1} [On] \to (A = \emptyset \leftrightarrow rank (A) = \emptyset)$

Metamath Proof Explorer

Theorem rankeq0b

Proof