Metamath Proof Explorer

Theorem rankr1ag

Description: A version of rankr1a that is suitable without assuming Regularity or Replacement. (Contributed by Mario Carneiro, 3-Jun-2013) (Revised by Mario Carneiro, 17-Nov-2014)

		Ref	Expression
	Assertion	rankr1ag	$⊢ (A \in ⋃ R_{1} [On] \land B \in dom R_{1}) \to (A \in R_{1} (B) \leftrightarrow rank (A) \in B)$

Proof

Step	Hyp	Ref	Expression
1		rankr1ai	$⊢ A \in R_{1} (B) \to rank (A) \in B$
2		r1dmlim	$⊢ Lim dom R_{1}$
3		limord	$⊢ Lim dom R_{1} \to Ord dom R_{1}$
4	2 3	ax-mp	$⊢ Ord dom R_{1}$
5		ordelord	$⊢ (Ord dom R_{1} \land B \in dom R_{1}) \to Ord B$
6	4 5	mpan	$⊢ B \in dom R_{1} \to Ord B$
7	6	adantl	$⊢ (A \in ⋃ R_{1} [On] \land B \in dom R_{1}) \to Ord B$
8		ordsucss	$⊢ Ord B \to (rank (A) \in B \to suc rank (A) \subseteq B)$
9	7 8	syl	$⊢ (A \in ⋃ R_{1} [On] \land B \in dom R_{1}) \to (rank (A) \in B \to suc rank (A) \subseteq B)$
10		rankidb	$⊢ A \in ⋃ R_{1} [On] \to A \in R_{1} (suc rank (A))$
11		elfvdm	$⊢ A \in R_{1} (suc rank (A)) \to suc rank (A) \in dom R_{1}$
12	10 11	syl	$⊢ A \in ⋃ R_{1} [On] \to suc rank (A) \in dom R_{1}$
13		r1ord3g	$⊢ (suc rank (A) \in dom R_{1} \land B \in dom R_{1}) \to (suc rank (A) \subseteq B \to R_{1} (suc rank (A)) \subseteq R_{1} (B))$
14	12 13	sylan	$⊢ (A \in ⋃ R_{1} [On] \land B \in dom R_{1}) \to (suc rank (A) \subseteq B \to R_{1} (suc rank (A)) \subseteq R_{1} (B))$
15	10	adantr	$⊢ (A \in ⋃ R_{1} [On] \land B \in dom R_{1}) \to A \in R_{1} (suc rank (A))$
16		ssel	$⊢ R_{1} (suc rank (A)) \subseteq R_{1} (B) \to (A \in R_{1} (suc rank (A)) \to A \in R_{1} (B))$
17	15 16	syl5com	$⊢ (A \in ⋃ R_{1} [On] \land B \in dom R_{1}) \to (R_{1} (suc rank (A)) \subseteq R_{1} (B) \to A \in R_{1} (B))$
18	9 14 17	3syld	$⊢ (A \in ⋃ R_{1} [On] \land B \in dom R_{1}) \to (rank (A) \in B \to A \in R_{1} (B))$
19	1 18	impbid2	$⊢ (A \in ⋃ R_{1} [On] \land B \in dom R_{1}) \to (A \in R_{1} (B) \leftrightarrow rank (A) \in B)$