Theorem rankuni2b

Description: The value of the rank function expressed recursively: the rank of a set is the smallest ordinal number containing the ranks of all members of the set. Proposition 9.17 of TakeutiZaring p. 79. (Contributed by Mario Carneiro, 8-Jun-2013)

	Ref	Expression
Assertion	rankuni2b	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( rank ‘ ∪ 𝐴 ) = ∪ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		uniwf	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ↔ ∪ 𝐴 ∈ ∪ ( 𝑅1 “ On ) )
2		rankval3b	⊢ ( ∪ 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( rank ‘ ∪ 𝐴 ) = ∩ { 𝑧 ∈ On ∣ ∀ 𝑦 ∈ ∪ 𝐴 ( rank ‘ 𝑦 ) ∈ 𝑧 } )
3	1 2	sylbi	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( rank ‘ ∪ 𝐴 ) = ∩ { 𝑧 ∈ On ∣ ∀ 𝑦 ∈ ∪ 𝐴 ( rank ‘ 𝑦 ) ∈ 𝑧 } )
4		eleq2	⊢ ( 𝑧 = ∪ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) → ( ( rank ‘ 𝑦 ) ∈ 𝑧 ↔ ( rank ‘ 𝑦 ) ∈ ∪ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) ) )
5	4	ralbidv	⊢ ( 𝑧 = ∪ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) → ( ∀ 𝑦 ∈ ∪ 𝐴 ( rank ‘ 𝑦 ) ∈ 𝑧 ↔ ∀ 𝑦 ∈ ∪ 𝐴 ( rank ‘ 𝑦 ) ∈ ∪ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) ) )
6		iuneq1	⊢ ( 𝑦 = 𝐴 → ∪ 𝑥 ∈ 𝑦 ( rank ‘ 𝑥 ) = ∪ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) )
7	6	eleq1d	⊢ ( 𝑦 = 𝐴 → ( ∪ 𝑥 ∈ 𝑦 ( rank ‘ 𝑥 ) ∈ On ↔ ∪ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) ∈ On ) )
8		vex	⊢ 𝑦 ∈ V
9		rankon	⊢ ( rank ‘ 𝑥 ) ∈ On
10	9	rgenw	⊢ ∀ 𝑥 ∈ 𝑦 ( rank ‘ 𝑥 ) ∈ On
11		iunon	⊢ ( ( 𝑦 ∈ V ∧ ∀ 𝑥 ∈ 𝑦 ( rank ‘ 𝑥 ) ∈ On ) → ∪ 𝑥 ∈ 𝑦 ( rank ‘ 𝑥 ) ∈ On )
12	8 10 11	mp2an	⊢ ∪ 𝑥 ∈ 𝑦 ( rank ‘ 𝑥 ) ∈ On
13	7 12	vtoclg	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ∪ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) ∈ On )
14		eluni2	⊢ ( 𝑦 ∈ ∪ 𝐴 ↔ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝑥 )
15		nfv	⊢ Ⅎ 𝑥 𝐴 ∈ ∪ ( 𝑅1 “ On )
16		nfiu1	⊢ Ⅎ 𝑥 ∪ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 )
17	16	nfel2	⊢ Ⅎ 𝑥 ( rank ‘ 𝑦 ) ∈ ∪ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 )
18		r1elssi	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → 𝐴 ⊆ ∪ ( 𝑅1 “ On ) )
19	18	sseld	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ∪ ( 𝑅1 “ On ) ) )
20		rankelb	⊢ ( 𝑥 ∈ ∪ ( 𝑅1 “ On ) → ( 𝑦 ∈ 𝑥 → ( rank ‘ 𝑦 ) ∈ ( rank ‘ 𝑥 ) ) )
21	19 20	syl6	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝑥 → ( rank ‘ 𝑦 ) ∈ ( rank ‘ 𝑥 ) ) ) )
22		ssiun2	⊢ ( 𝑥 ∈ 𝐴 → ( rank ‘ 𝑥 ) ⊆ ∪ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) )
23	22	sseld	⊢ ( 𝑥 ∈ 𝐴 → ( ( rank ‘ 𝑦 ) ∈ ( rank ‘ 𝑥 ) → ( rank ‘ 𝑦 ) ∈ ∪ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) ) )
24	23	a1i	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( 𝑥 ∈ 𝐴 → ( ( rank ‘ 𝑦 ) ∈ ( rank ‘ 𝑥 ) → ( rank ‘ 𝑦 ) ∈ ∪ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) ) ) )
25	21 24	syldd	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝑥 → ( rank ‘ 𝑦 ) ∈ ∪ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) ) ) )
26	15 17 25	rexlimd	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝑥 → ( rank ‘ 𝑦 ) ∈ ∪ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) ) )
27	14 26	biimtrid	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( 𝑦 ∈ ∪ 𝐴 → ( rank ‘ 𝑦 ) ∈ ∪ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) ) )
28	27	ralrimiv	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ∀ 𝑦 ∈ ∪ 𝐴 ( rank ‘ 𝑦 ) ∈ ∪ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) )
29	5 13 28	elrabd	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ∪ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) ∈ { 𝑧 ∈ On ∣ ∀ 𝑦 ∈ ∪ 𝐴 ( rank ‘ 𝑦 ) ∈ 𝑧 } )
30		intss1	⊢ ( ∪ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) ∈ { 𝑧 ∈ On ∣ ∀ 𝑦 ∈ ∪ 𝐴 ( rank ‘ 𝑦 ) ∈ 𝑧 } → ∩ { 𝑧 ∈ On ∣ ∀ 𝑦 ∈ ∪ 𝐴 ( rank ‘ 𝑦 ) ∈ 𝑧 } ⊆ ∪ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) )
31	29 30	syl	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ∩ { 𝑧 ∈ On ∣ ∀ 𝑦 ∈ ∪ 𝐴 ( rank ‘ 𝑦 ) ∈ 𝑧 } ⊆ ∪ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) )
32	3 31	eqsstrd	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( rank ‘ ∪ 𝐴 ) ⊆ ∪ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) )
33	1	biimpi	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ∪ 𝐴 ∈ ∪ ( 𝑅1 “ On ) )
34		elssuni	⊢ ( 𝑥 ∈ 𝐴 → 𝑥 ⊆ ∪ 𝐴 )
35		rankssb	⊢ ( ∪ 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( 𝑥 ⊆ ∪ 𝐴 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ ∪ 𝐴 ) ) )
36	33 34 35	syl2im	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( 𝑥 ∈ 𝐴 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ ∪ 𝐴 ) ) )
37	36	ralrimiv	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ∀ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ ∪ 𝐴 ) )
38		iunss	⊢ ( ∪ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ ∪ 𝐴 ) ↔ ∀ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ ∪ 𝐴 ) )
39	37 38	sylibr	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ∪ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ ∪ 𝐴 ) )
40	32 39	eqssd	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( rank ‘ ∪ 𝐴 ) = ∪ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) )