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		r1funlim	$⊢ (Fun R_{1} \land Lim dom R_{1})$
3	2	simpri	$⊢ Lim dom R_{1}$
4		limord	$⊢ Lim dom R_{1} \to Ord dom R_{1}$
5	3 4	ax-mp	$⊢ Ord dom R_{1}$
6		ordelord	$⊢ (Ord dom R_{1} \land B \in dom R_{1}) \to Ord B$
7	5 6	mpan	$⊢ B \in dom R_{1} \to Ord B$
8	7	adantl	$⊢ (A \in ⋃ R_{1} [On] \land B \in dom R_{1}) \to Ord B$
9		ordsucss	$⊢ Ord B \to (rank (A) \in B \to suc rank (A) \subseteq B)$
10	8 9	syl	$⊢ (A \in ⋃ R_{1} [On] \land B \in dom R_{1}) \to (rank (A) \in B \to suc rank (A) \subseteq B)$
11		rankidb	$⊢ A \in ⋃ R_{1} [On] \to A \in R_{1} (suc rank (A))$
12		elfvdm	$⊢ A \in R_{1} (suc rank (A)) \to suc rank (A) \in dom R_{1}$
13	11 12	syl	$⊢ A \in ⋃ R_{1} [On] \to suc rank (A) \in dom R_{1}$
14		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))$
15	13 14	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))$
16	11	adantr	$⊢ (A \in ⋃ R_{1} [On] \land B \in dom R_{1}) \to A \in R_{1} (suc rank (A))$
17		ssel	$⊢ R_{1} (suc rank (A)) \subseteq R_{1} (B) \to (A \in R_{1} (suc rank (A)) \to A \in R_{1} (B))$
18	16 17	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))$
19	10 15 18	3syld	$⊢ (A \in ⋃ R_{1} [On] \land B \in dom R_{1}) \to (rank (A) \in B \to A \in R_{1} (B))$
20	1 19	impbid2	$⊢ (A \in ⋃ R_{1} [On] \land B \in dom R_{1}) \to (A \in R_{1} (B) \leftrightarrow rank (A) \in B)$

Metamath Proof Explorer

Theorem rankr1ag

Proof