scottrankd

Description: Rank of a nonempty Scott's trick set. (Contributed by Rohan Ridenour, 11-Aug-2023)

		Ref	Expression
	Hypothesis	scottrankd.1	$⊢ φ \to B \in Scott A$
	Assertion	scottrankd	$⊢ φ \to rank (Scott A) = suc rank (B)$

Step	Hyp	Ref	Expression
1		scottrankd.1	$⊢ φ \to B \in Scott A$
2		scottex2	$⊢ Scott A \in V$
3	2	rankval4	$⊢ rank (Scott A) = ⋃_{x \in Scott A} suc rank (x)$
4	3	a1i	$⊢ φ \to rank (Scott A) = ⋃_{x \in Scott A} suc rank (x)$
5	1	adantr	$⊢ (φ \land x \in Scott A) \to B \in Scott A$
6		simpr	$⊢ (φ \land x \in Scott A) \to x \in Scott A$
7	5 6	scottelrankd	$⊢ (φ \land x \in Scott A) \to rank (B) \subseteq rank (x)$
8	6 5	scottelrankd	$⊢ (φ \land x \in Scott A) \to rank (x) \subseteq rank (B)$
9	7 8	eqssd	$⊢ (φ \land x \in Scott A) \to rank (B) = rank (x)$
10	9	suceqd	$⊢ (φ \land x \in Scott A) \to suc rank (B) = suc rank (x)$
11	10	iuneq2dv	$⊢ φ \to ⋃_{x \in Scott A} suc rank (B) = ⋃_{x \in Scott A} suc rank (x)$
12	1	ne0d	$⊢ φ \to Scott A \neq \emptyset$
13		iunconst	$⊢ Scott A \neq \emptyset \to ⋃_{x \in Scott A} suc rank (B) = suc rank (B)$
14	12 13	syl	$⊢ φ \to ⋃_{x \in Scott A} suc rank (B) = suc rank (B)$
15	4 11 14	3eqtr2d	$⊢ φ \to rank (Scott A) = suc rank (B)$

Metamath Proof Explorer