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		r1dmlim	$⊢ Lim dom R_{1}$
3		limomss	$⊢ Lim dom R_{1} \to ω \subseteq dom R_{1}$
4	2 3	ax-mp	$⊢ ω \subseteq dom R_{1}$
5		peano1	$⊢ \emptyset \in ω$
6	4 5	sselii	$⊢ \emptyset \in dom R_{1}$
7		rankonid	$⊢ \emptyset \in dom R_{1} \leftrightarrow rank (\emptyset) = \emptyset$
8	6 7	mpbi	$⊢ rank (\emptyset) = \emptyset$
9	1 8	eqtrdi	$⊢ A = \emptyset \to rank (A) = \emptyset$
10		eqimss	$⊢ rank (A) = \emptyset \to rank (A) \subseteq \emptyset$
11	10	adantl	$⊢ (A \in ⋃ R_{1} [On] \land rank (A) = \emptyset) \to rank (A) \subseteq \emptyset$
12		simpl	$⊢ (A \in ⋃ R_{1} [On] \land rank (A) = \emptyset) \to A \in ⋃ R_{1} [On]$
13		rankr1bg	$⊢ (A \in ⋃ R_{1} [On] \land \emptyset \in dom R_{1}) \to (A \subseteq R_{1} (\emptyset) \leftrightarrow rank (A) \subseteq \emptyset)$
14	12 6 13	sylancl	$⊢ (A \in ⋃ R_{1} [On] \land rank (A) = \emptyset) \to (A \subseteq R_{1} (\emptyset) \leftrightarrow rank (A) \subseteq \emptyset)$
15	11 14	mpbird	$⊢ (A \in ⋃ R_{1} [On] \land rank (A) = \emptyset) \to A \subseteq R_{1} (\emptyset)$
16		r10	$⊢ R_{1} (\emptyset) = \emptyset$
17	15 16	sseqtrdi	$⊢ (A \in ⋃ R_{1} [On] \land rank (A) = \emptyset) \to A \subseteq \emptyset$
18		ss0	$⊢ A \subseteq \emptyset \to A = \emptyset$
19	17 18	syl	$⊢ (A \in ⋃ R_{1} [On] \land rank (A) = \emptyset) \to A = \emptyset$
20	19	ex	$⊢ A \in ⋃ R_{1} [On] \to (rank (A) = \emptyset \to A = \emptyset)$
21	9 20	impbid2	$⊢ A \in ⋃ R_{1} [On] \to (A = \emptyset \leftrightarrow rank (A) = \emptyset)$

Metamath Proof Explorer

Theorem rankeq0b

Proof