Theorem dfac12r

Description: The axiom of choice holds iff every ordinal has a well-orderable powerset. This version of dfac12 does not assume the Axiom of Regularity. (Contributed by Mario Carneiro, 29-May-2015)

	Ref	Expression
Assertion	dfac12r	⊢ ( ∀ 𝑥 ∈ On 𝒫 𝑥 ∈ dom card ↔ ∪ ( 𝑅1 “ On ) ⊆ dom card )

Proof

Step	Hyp	Ref	Expression
1		rankwflemb	⊢ ( 𝑦 ∈ ∪ ( 𝑅1 “ On ) ↔ ∃ 𝑧 ∈ On 𝑦 ∈ ( 𝑅1 ‘ suc 𝑧 ) )
2		harcl	⊢ ( har ‘ ( 𝑅1 ‘ 𝑧 ) ) ∈ On
3		pweq	⊢ ( 𝑥 = ( har ‘ ( 𝑅1 ‘ 𝑧 ) ) → 𝒫 𝑥 = 𝒫 ( har ‘ ( 𝑅1 ‘ 𝑧 ) ) )
4	3	eleq1d	⊢ ( 𝑥 = ( har ‘ ( 𝑅1 ‘ 𝑧 ) ) → ( 𝒫 𝑥 ∈ dom card ↔ 𝒫 ( har ‘ ( 𝑅1 ‘ 𝑧 ) ) ∈ dom card ) )
5	4	rspcv	⊢ ( ( har ‘ ( 𝑅1 ‘ 𝑧 ) ) ∈ On → ( ∀ 𝑥 ∈ On 𝒫 𝑥 ∈ dom card → 𝒫 ( har ‘ ( 𝑅1 ‘ 𝑧 ) ) ∈ dom card ) )
6	2 5	ax-mp	⊢ ( ∀ 𝑥 ∈ On 𝒫 𝑥 ∈ dom card → 𝒫 ( har ‘ ( 𝑅1 ‘ 𝑧 ) ) ∈ dom card )
7		cardid2	⊢ ( 𝒫 ( har ‘ ( 𝑅1 ‘ 𝑧 ) ) ∈ dom card → ( card ‘ 𝒫 ( har ‘ ( 𝑅1 ‘ 𝑧 ) ) ) ≈ 𝒫 ( har ‘ ( 𝑅1 ‘ 𝑧 ) ) )
8		ensym	⊢ ( ( card ‘ 𝒫 ( har ‘ ( 𝑅1 ‘ 𝑧 ) ) ) ≈ 𝒫 ( har ‘ ( 𝑅1 ‘ 𝑧 ) ) → 𝒫 ( har ‘ ( 𝑅1 ‘ 𝑧 ) ) ≈ ( card ‘ 𝒫 ( har ‘ ( 𝑅1 ‘ 𝑧 ) ) ) )
9		bren	⊢ ( 𝒫 ( har ‘ ( 𝑅1 ‘ 𝑧 ) ) ≈ ( card ‘ 𝒫 ( har ‘ ( 𝑅1 ‘ 𝑧 ) ) ) ↔ ∃ 𝑓 𝑓 : 𝒫 ( har ‘ ( 𝑅1 ‘ 𝑧 ) ) –1-1-onto→ ( card ‘ 𝒫 ( har ‘ ( 𝑅1 ‘ 𝑧 ) ) ) )
10		simpr	⊢ ( ( 𝑓 : 𝒫 ( har ‘ ( 𝑅1 ‘ 𝑧 ) ) –1-1-onto→ ( card ‘ 𝒫 ( har ‘ ( 𝑅1 ‘ 𝑧 ) ) ) ∧ 𝑧 ∈ On ) → 𝑧 ∈ On )
11		f1of1	⊢ ( 𝑓 : 𝒫 ( har ‘ ( 𝑅1 ‘ 𝑧 ) ) –1-1-onto→ ( card ‘ 𝒫 ( har ‘ ( 𝑅1 ‘ 𝑧 ) ) ) → 𝑓 : 𝒫 ( har ‘ ( 𝑅1 ‘ 𝑧 ) ) –1-1→ ( card ‘ 𝒫 ( har ‘ ( 𝑅1 ‘ 𝑧 ) ) ) )
12	11	adantr	⊢ ( ( 𝑓 : 𝒫 ( har ‘ ( 𝑅1 ‘ 𝑧 ) ) –1-1-onto→ ( card ‘ 𝒫 ( har ‘ ( 𝑅1 ‘ 𝑧 ) ) ) ∧ 𝑧 ∈ On ) → 𝑓 : 𝒫 ( har ‘ ( 𝑅1 ‘ 𝑧 ) ) –1-1→ ( card ‘ 𝒫 ( har ‘ ( 𝑅1 ‘ 𝑧 ) ) ) )
13		cardon	⊢ ( card ‘ 𝒫 ( har ‘ ( 𝑅1 ‘ 𝑧 ) ) ) ∈ On
14	13	onssi	⊢ ( card ‘ 𝒫 ( har ‘ ( 𝑅1 ‘ 𝑧 ) ) ) ⊆ On
15		f1ss	⊢ ( ( 𝑓 : 𝒫 ( har ‘ ( 𝑅1 ‘ 𝑧 ) ) –1-1→ ( card ‘ 𝒫 ( har ‘ ( 𝑅1 ‘ 𝑧 ) ) ) ∧ ( card ‘ 𝒫 ( har ‘ ( 𝑅1 ‘ 𝑧 ) ) ) ⊆ On ) → 𝑓 : 𝒫 ( har ‘ ( 𝑅1 ‘ 𝑧 ) ) –1-1→ On )
16	12 14 15	sylancl	⊢ ( ( 𝑓 : 𝒫 ( har ‘ ( 𝑅1 ‘ 𝑧 ) ) –1-1-onto→ ( card ‘ 𝒫 ( har ‘ ( 𝑅1 ‘ 𝑧 ) ) ) ∧ 𝑧 ∈ On ) → 𝑓 : 𝒫 ( har ‘ ( 𝑅1 ‘ 𝑧 ) ) –1-1→ On )
17		fveq2	⊢ ( 𝑦 = 𝑏 → ( rank ‘ 𝑦 ) = ( rank ‘ 𝑏 ) )
18	17	oveq2d	⊢ ( 𝑦 = 𝑏 → ( suc ∪ ran ∪ ran 𝑥 ·o ( rank ‘ 𝑦 ) ) = ( suc ∪ ran ∪ ran 𝑥 ·o ( rank ‘ 𝑏 ) ) )
19		suceq	⊢ ( ( rank ‘ 𝑦 ) = ( rank ‘ 𝑏 ) → suc ( rank ‘ 𝑦 ) = suc ( rank ‘ 𝑏 ) )
20	17 19	syl	⊢ ( 𝑦 = 𝑏 → suc ( rank ‘ 𝑦 ) = suc ( rank ‘ 𝑏 ) )
21	20	fveq2d	⊢ ( 𝑦 = 𝑏 → ( 𝑥 ‘ suc ( rank ‘ 𝑦 ) ) = ( 𝑥 ‘ suc ( rank ‘ 𝑏 ) ) )
22		id	⊢ ( 𝑦 = 𝑏 → 𝑦 = 𝑏 )
23	21 22	fveq12d	⊢ ( 𝑦 = 𝑏 → ( ( 𝑥 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) = ( ( 𝑥 ‘ suc ( rank ‘ 𝑏 ) ) ‘ 𝑏 ) )
24	18 23	oveq12d	⊢ ( 𝑦 = 𝑏 → ( ( suc ∪ ran ∪ ran 𝑥 ·o ( rank ‘ 𝑦 ) ) +o ( ( 𝑥 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) = ( ( suc ∪ ran ∪ ran 𝑥 ·o ( rank ‘ 𝑏 ) ) +o ( ( 𝑥 ‘ suc ( rank ‘ 𝑏 ) ) ‘ 𝑏 ) ) )
25		imaeq2	⊢ ( 𝑦 = 𝑏 → ( ( ◡ OrdIso ( E , ran ( 𝑥 ‘ ∪ dom 𝑥 ) ) ∘ ( 𝑥 ‘ ∪ dom 𝑥 ) ) “ 𝑦 ) = ( ( ◡ OrdIso ( E , ran ( 𝑥 ‘ ∪ dom 𝑥 ) ) ∘ ( 𝑥 ‘ ∪ dom 𝑥 ) ) “ 𝑏 ) )
26	25	fveq2d	⊢ ( 𝑦 = 𝑏 → ( 𝑓 ‘ ( ( ◡ OrdIso ( E , ran ( 𝑥 ‘ ∪ dom 𝑥 ) ) ∘ ( 𝑥 ‘ ∪ dom 𝑥 ) ) “ 𝑦 ) ) = ( 𝑓 ‘ ( ( ◡ OrdIso ( E , ran ( 𝑥 ‘ ∪ dom 𝑥 ) ) ∘ ( 𝑥 ‘ ∪ dom 𝑥 ) ) “ 𝑏 ) ) )
27	24 26	ifeq12d	⊢ ( 𝑦 = 𝑏 → if ( dom 𝑥 = ∪ dom 𝑥 , ( ( suc ∪ ran ∪ ran 𝑥 ·o ( rank ‘ 𝑦 ) ) +o ( ( 𝑥 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) , ( 𝑓 ‘ ( ( ◡ OrdIso ( E , ran ( 𝑥 ‘ ∪ dom 𝑥 ) ) ∘ ( 𝑥 ‘ ∪ dom 𝑥 ) ) “ 𝑦 ) ) ) = if ( dom 𝑥 = ∪ dom 𝑥 , ( ( suc ∪ ran ∪ ran 𝑥 ·o ( rank ‘ 𝑏 ) ) +o ( ( 𝑥 ‘ suc ( rank ‘ 𝑏 ) ) ‘ 𝑏 ) ) , ( 𝑓 ‘ ( ( ◡ OrdIso ( E , ran ( 𝑥 ‘ ∪ dom 𝑥 ) ) ∘ ( 𝑥 ‘ ∪ dom 𝑥 ) ) “ 𝑏 ) ) ) )
28	27	cbvmptv	⊢ ( 𝑦 ∈ ( 𝑅1 ‘ dom 𝑥 ) ↦ if ( dom 𝑥 = ∪ dom 𝑥 , ( ( suc ∪ ran ∪ ran 𝑥 ·o ( rank ‘ 𝑦 ) ) +o ( ( 𝑥 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) , ( 𝑓 ‘ ( ( ◡ OrdIso ( E , ran ( 𝑥 ‘ ∪ dom 𝑥 ) ) ∘ ( 𝑥 ‘ ∪ dom 𝑥 ) ) “ 𝑦 ) ) ) ) = ( 𝑏 ∈ ( 𝑅1 ‘ dom 𝑥 ) ↦ if ( dom 𝑥 = ∪ dom 𝑥 , ( ( suc ∪ ran ∪ ran 𝑥 ·o ( rank ‘ 𝑏 ) ) +o ( ( 𝑥 ‘ suc ( rank ‘ 𝑏 ) ) ‘ 𝑏 ) ) , ( 𝑓 ‘ ( ( ◡ OrdIso ( E , ran ( 𝑥 ‘ ∪ dom 𝑥 ) ) ∘ ( 𝑥 ‘ ∪ dom 𝑥 ) ) “ 𝑏 ) ) ) )
29		dmeq	⊢ ( 𝑥 = 𝑎 → dom 𝑥 = dom 𝑎 )
30	29	fveq2d	⊢ ( 𝑥 = 𝑎 → ( 𝑅1 ‘ dom 𝑥 ) = ( 𝑅1 ‘ dom 𝑎 ) )
31	29	unieqd	⊢ ( 𝑥 = 𝑎 → ∪ dom 𝑥 = ∪ dom 𝑎 )
32	29 31	eqeq12d	⊢ ( 𝑥 = 𝑎 → ( dom 𝑥 = ∪ dom 𝑥 ↔ dom 𝑎 = ∪ dom 𝑎 ) )
33		rneq	⊢ ( 𝑥 = 𝑎 → ran 𝑥 = ran 𝑎 )
34	33	unieqd	⊢ ( 𝑥 = 𝑎 → ∪ ran 𝑥 = ∪ ran 𝑎 )
35	34	rneqd	⊢ ( 𝑥 = 𝑎 → ran ∪ ran 𝑥 = ran ∪ ran 𝑎 )
36	35	unieqd	⊢ ( 𝑥 = 𝑎 → ∪ ran ∪ ran 𝑥 = ∪ ran ∪ ran 𝑎 )
37		suceq	⊢ ( ∪ ran ∪ ran 𝑥 = ∪ ran ∪ ran 𝑎 → suc ∪ ran ∪ ran 𝑥 = suc ∪ ran ∪ ran 𝑎 )
38	36 37	syl	⊢ ( 𝑥 = 𝑎 → suc ∪ ran ∪ ran 𝑥 = suc ∪ ran ∪ ran 𝑎 )
39	38	oveq1d	⊢ ( 𝑥 = 𝑎 → ( suc ∪ ran ∪ ran 𝑥 ·o ( rank ‘ 𝑏 ) ) = ( suc ∪ ran ∪ ran 𝑎 ·o ( rank ‘ 𝑏 ) ) )
40		fveq1	⊢ ( 𝑥 = 𝑎 → ( 𝑥 ‘ suc ( rank ‘ 𝑏 ) ) = ( 𝑎 ‘ suc ( rank ‘ 𝑏 ) ) )
41	40	fveq1d	⊢ ( 𝑥 = 𝑎 → ( ( 𝑥 ‘ suc ( rank ‘ 𝑏 ) ) ‘ 𝑏 ) = ( ( 𝑎 ‘ suc ( rank ‘ 𝑏 ) ) ‘ 𝑏 ) )
42	39 41	oveq12d	⊢ ( 𝑥 = 𝑎 → ( ( suc ∪ ran ∪ ran 𝑥 ·o ( rank ‘ 𝑏 ) ) +o ( ( 𝑥 ‘ suc ( rank ‘ 𝑏 ) ) ‘ 𝑏 ) ) = ( ( suc ∪ ran ∪ ran 𝑎 ·o ( rank ‘ 𝑏 ) ) +o ( ( 𝑎 ‘ suc ( rank ‘ 𝑏 ) ) ‘ 𝑏 ) ) )
43		id	⊢ ( 𝑥 = 𝑎 → 𝑥 = 𝑎 )
44	43 31	fveq12d	⊢ ( 𝑥 = 𝑎 → ( 𝑥 ‘ ∪ dom 𝑥 ) = ( 𝑎 ‘ ∪ dom 𝑎 ) )
45	44	rneqd	⊢ ( 𝑥 = 𝑎 → ran ( 𝑥 ‘ ∪ dom 𝑥 ) = ran ( 𝑎 ‘ ∪ dom 𝑎 ) )
46		oieq2	⊢ ( ran ( 𝑥 ‘ ∪ dom 𝑥 ) = ran ( 𝑎 ‘ ∪ dom 𝑎 ) → OrdIso ( E , ran ( 𝑥 ‘ ∪ dom 𝑥 ) ) = OrdIso ( E , ran ( 𝑎 ‘ ∪ dom 𝑎 ) ) )
47	45 46	syl	⊢ ( 𝑥 = 𝑎 → OrdIso ( E , ran ( 𝑥 ‘ ∪ dom 𝑥 ) ) = OrdIso ( E , ran ( 𝑎 ‘ ∪ dom 𝑎 ) ) )
48	47	cnveqd	⊢ ( 𝑥 = 𝑎 → ◡ OrdIso ( E , ran ( 𝑥 ‘ ∪ dom 𝑥 ) ) = ◡ OrdIso ( E , ran ( 𝑎 ‘ ∪ dom 𝑎 ) ) )
49	48 44	coeq12d	⊢ ( 𝑥 = 𝑎 → ( ◡ OrdIso ( E , ran ( 𝑥 ‘ ∪ dom 𝑥 ) ) ∘ ( 𝑥 ‘ ∪ dom 𝑥 ) ) = ( ◡ OrdIso ( E , ran ( 𝑎 ‘ ∪ dom 𝑎 ) ) ∘ ( 𝑎 ‘ ∪ dom 𝑎 ) ) )
50	49	imaeq1d	⊢ ( 𝑥 = 𝑎 → ( ( ◡ OrdIso ( E , ran ( 𝑥 ‘ ∪ dom 𝑥 ) ) ∘ ( 𝑥 ‘ ∪ dom 𝑥 ) ) “ 𝑏 ) = ( ( ◡ OrdIso ( E , ran ( 𝑎 ‘ ∪ dom 𝑎 ) ) ∘ ( 𝑎 ‘ ∪ dom 𝑎 ) ) “ 𝑏 ) )
51	50	fveq2d	⊢ ( 𝑥 = 𝑎 → ( 𝑓 ‘ ( ( ◡ OrdIso ( E , ran ( 𝑥 ‘ ∪ dom 𝑥 ) ) ∘ ( 𝑥 ‘ ∪ dom 𝑥 ) ) “ 𝑏 ) ) = ( 𝑓 ‘ ( ( ◡ OrdIso ( E , ran ( 𝑎 ‘ ∪ dom 𝑎 ) ) ∘ ( 𝑎 ‘ ∪ dom 𝑎 ) ) “ 𝑏 ) ) )
52	32 42 51	ifbieq12d	⊢ ( 𝑥 = 𝑎 → if ( dom 𝑥 = ∪ dom 𝑥 , ( ( suc ∪ ran ∪ ran 𝑥 ·o ( rank ‘ 𝑏 ) ) +o ( ( 𝑥 ‘ suc ( rank ‘ 𝑏 ) ) ‘ 𝑏 ) ) , ( 𝑓 ‘ ( ( ◡ OrdIso ( E , ran ( 𝑥 ‘ ∪ dom 𝑥 ) ) ∘ ( 𝑥 ‘ ∪ dom 𝑥 ) ) “ 𝑏 ) ) ) = if ( dom 𝑎 = ∪ dom 𝑎 , ( ( suc ∪ ran ∪ ran 𝑎 ·o ( rank ‘ 𝑏 ) ) +o ( ( 𝑎 ‘ suc ( rank ‘ 𝑏 ) ) ‘ 𝑏 ) ) , ( 𝑓 ‘ ( ( ◡ OrdIso ( E , ran ( 𝑎 ‘ ∪ dom 𝑎 ) ) ∘ ( 𝑎 ‘ ∪ dom 𝑎 ) ) “ 𝑏 ) ) ) )
53	30 52	mpteq12dv	⊢ ( 𝑥 = 𝑎 → ( 𝑏 ∈ ( 𝑅1 ‘ dom 𝑥 ) ↦ if ( dom 𝑥 = ∪ dom 𝑥 , ( ( suc ∪ ran ∪ ran 𝑥 ·o ( rank ‘ 𝑏 ) ) +o ( ( 𝑥 ‘ suc ( rank ‘ 𝑏 ) ) ‘ 𝑏 ) ) , ( 𝑓 ‘ ( ( ◡ OrdIso ( E , ran ( 𝑥 ‘ ∪ dom 𝑥 ) ) ∘ ( 𝑥 ‘ ∪ dom 𝑥 ) ) “ 𝑏 ) ) ) ) = ( 𝑏 ∈ ( 𝑅1 ‘ dom 𝑎 ) ↦ if ( dom 𝑎 = ∪ dom 𝑎 , ( ( suc ∪ ran ∪ ran 𝑎 ·o ( rank ‘ 𝑏 ) ) +o ( ( 𝑎 ‘ suc ( rank ‘ 𝑏 ) ) ‘ 𝑏 ) ) , ( 𝑓 ‘ ( ( ◡ OrdIso ( E , ran ( 𝑎 ‘ ∪ dom 𝑎 ) ) ∘ ( 𝑎 ‘ ∪ dom 𝑎 ) ) “ 𝑏 ) ) ) ) )
54	28 53	eqtrid	⊢ ( 𝑥 = 𝑎 → ( 𝑦 ∈ ( 𝑅1 ‘ dom 𝑥 ) ↦ if ( dom 𝑥 = ∪ dom 𝑥 , ( ( suc ∪ ran ∪ ran 𝑥 ·o ( rank ‘ 𝑦 ) ) +o ( ( 𝑥 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) , ( 𝑓 ‘ ( ( ◡ OrdIso ( E , ran ( 𝑥 ‘ ∪ dom 𝑥 ) ) ∘ ( 𝑥 ‘ ∪ dom 𝑥 ) ) “ 𝑦 ) ) ) ) = ( 𝑏 ∈ ( 𝑅1 ‘ dom 𝑎 ) ↦ if ( dom 𝑎 = ∪ dom 𝑎 , ( ( suc ∪ ran ∪ ran 𝑎 ·o ( rank ‘ 𝑏 ) ) +o ( ( 𝑎 ‘ suc ( rank ‘ 𝑏 ) ) ‘ 𝑏 ) ) , ( 𝑓 ‘ ( ( ◡ OrdIso ( E , ran ( 𝑎 ‘ ∪ dom 𝑎 ) ) ∘ ( 𝑎 ‘ ∪ dom 𝑎 ) ) “ 𝑏 ) ) ) ) )
55	54	cbvmptv	⊢ ( 𝑥 ∈ V ↦ ( 𝑦 ∈ ( 𝑅1 ‘ dom 𝑥 ) ↦ if ( dom 𝑥 = ∪ dom 𝑥 , ( ( suc ∪ ran ∪ ran 𝑥 ·o ( rank ‘ 𝑦 ) ) +o ( ( 𝑥 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) , ( 𝑓 ‘ ( ( ◡ OrdIso ( E , ran ( 𝑥 ‘ ∪ dom 𝑥 ) ) ∘ ( 𝑥 ‘ ∪ dom 𝑥 ) ) “ 𝑦 ) ) ) ) ) = ( 𝑎 ∈ V ↦ ( 𝑏 ∈ ( 𝑅1 ‘ dom 𝑎 ) ↦ if ( dom 𝑎 = ∪ dom 𝑎 , ( ( suc ∪ ran ∪ ran 𝑎 ·o ( rank ‘ 𝑏 ) ) +o ( ( 𝑎 ‘ suc ( rank ‘ 𝑏 ) ) ‘ 𝑏 ) ) , ( 𝑓 ‘ ( ( ◡ OrdIso ( E , ran ( 𝑎 ‘ ∪ dom 𝑎 ) ) ∘ ( 𝑎 ‘ ∪ dom 𝑎 ) ) “ 𝑏 ) ) ) ) )
56		recseq	⊢ ( ( 𝑥 ∈ V ↦ ( 𝑦 ∈ ( 𝑅1 ‘ dom 𝑥 ) ↦ if ( dom 𝑥 = ∪ dom 𝑥 , ( ( suc ∪ ran ∪ ran 𝑥 ·o ( rank ‘ 𝑦 ) ) +o ( ( 𝑥 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) , ( 𝑓 ‘ ( ( ◡ OrdIso ( E , ran ( 𝑥 ‘ ∪ dom 𝑥 ) ) ∘ ( 𝑥 ‘ ∪ dom 𝑥 ) ) “ 𝑦 ) ) ) ) ) = ( 𝑎 ∈ V ↦ ( 𝑏 ∈ ( 𝑅1 ‘ dom 𝑎 ) ↦ if ( dom 𝑎 = ∪ dom 𝑎 , ( ( suc ∪ ran ∪ ran 𝑎 ·o ( rank ‘ 𝑏 ) ) +o ( ( 𝑎 ‘ suc ( rank ‘ 𝑏 ) ) ‘ 𝑏 ) ) , ( 𝑓 ‘ ( ( ◡ OrdIso ( E , ran ( 𝑎 ‘ ∪ dom 𝑎 ) ) ∘ ( 𝑎 ‘ ∪ dom 𝑎 ) ) “ 𝑏 ) ) ) ) ) → recs ( ( 𝑥 ∈ V ↦ ( 𝑦 ∈ ( 𝑅1 ‘ dom 𝑥 ) ↦ if ( dom 𝑥 = ∪ dom 𝑥 , ( ( suc ∪ ran ∪ ran 𝑥 ·o ( rank ‘ 𝑦 ) ) +o ( ( 𝑥 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) , ( 𝑓 ‘ ( ( ◡ OrdIso ( E , ran ( 𝑥 ‘ ∪ dom 𝑥 ) ) ∘ ( 𝑥 ‘ ∪ dom 𝑥 ) ) “ 𝑦 ) ) ) ) ) ) = recs ( ( 𝑎 ∈ V ↦ ( 𝑏 ∈ ( 𝑅1 ‘ dom 𝑎 ) ↦ if ( dom 𝑎 = ∪ dom 𝑎 , ( ( suc ∪ ran ∪ ran 𝑎 ·o ( rank ‘ 𝑏 ) ) +o ( ( 𝑎 ‘ suc ( rank ‘ 𝑏 ) ) ‘ 𝑏 ) ) , ( 𝑓 ‘ ( ( ◡ OrdIso ( E , ran ( 𝑎 ‘ ∪ dom 𝑎 ) ) ∘ ( 𝑎 ‘ ∪ dom 𝑎 ) ) “ 𝑏 ) ) ) ) ) ) )
57	55 56	ax-mp	⊢ recs ( ( 𝑥 ∈ V ↦ ( 𝑦 ∈ ( 𝑅1 ‘ dom 𝑥 ) ↦ if ( dom 𝑥 = ∪ dom 𝑥 , ( ( suc ∪ ran ∪ ran 𝑥 ·o ( rank ‘ 𝑦 ) ) +o ( ( 𝑥 ‘ suc ( rank ‘ 𝑦 ) ) ‘ 𝑦 ) ) , ( 𝑓 ‘ ( ( ◡ OrdIso ( E , ran ( 𝑥 ‘ ∪ dom 𝑥 ) ) ∘ ( 𝑥 ‘ ∪ dom 𝑥 ) ) “ 𝑦 ) ) ) ) ) ) = recs ( ( 𝑎 ∈ V ↦ ( 𝑏 ∈ ( 𝑅1 ‘ dom 𝑎 ) ↦ if ( dom 𝑎 = ∪ dom 𝑎 , ( ( suc ∪ ran ∪ ran 𝑎 ·o ( rank ‘ 𝑏 ) ) +o ( ( 𝑎 ‘ suc ( rank ‘ 𝑏 ) ) ‘ 𝑏 ) ) , ( 𝑓 ‘ ( ( ◡ OrdIso ( E , ran ( 𝑎 ‘ ∪ dom 𝑎 ) ) ∘ ( 𝑎 ‘ ∪ dom 𝑎 ) ) “ 𝑏 ) ) ) ) ) )
58	10 16 57	dfac12lem3	⊢ ( ( 𝑓 : 𝒫 ( har ‘ ( 𝑅1 ‘ 𝑧 ) ) –1-1-onto→ ( card ‘ 𝒫 ( har ‘ ( 𝑅1 ‘ 𝑧 ) ) ) ∧ 𝑧 ∈ On ) → ( 𝑅1 ‘ 𝑧 ) ∈ dom card )
59	58	ex	⊢ ( 𝑓 : 𝒫 ( har ‘ ( 𝑅1 ‘ 𝑧 ) ) –1-1-onto→ ( card ‘ 𝒫 ( har ‘ ( 𝑅1 ‘ 𝑧 ) ) ) → ( 𝑧 ∈ On → ( 𝑅1 ‘ 𝑧 ) ∈ dom card ) )
60	59	exlimiv	⊢ ( ∃ 𝑓 𝑓 : 𝒫 ( har ‘ ( 𝑅1 ‘ 𝑧 ) ) –1-1-onto→ ( card ‘ 𝒫 ( har ‘ ( 𝑅1 ‘ 𝑧 ) ) ) → ( 𝑧 ∈ On → ( 𝑅1 ‘ 𝑧 ) ∈ dom card ) )
61	9 60	sylbi	⊢ ( 𝒫 ( har ‘ ( 𝑅1 ‘ 𝑧 ) ) ≈ ( card ‘ 𝒫 ( har ‘ ( 𝑅1 ‘ 𝑧 ) ) ) → ( 𝑧 ∈ On → ( 𝑅1 ‘ 𝑧 ) ∈ dom card ) )
62	6 7 8 61	4syl	⊢ ( ∀ 𝑥 ∈ On 𝒫 𝑥 ∈ dom card → ( 𝑧 ∈ On → ( 𝑅1 ‘ 𝑧 ) ∈ dom card ) )
63	62	imp	⊢ ( ( ∀ 𝑥 ∈ On 𝒫 𝑥 ∈ dom card ∧ 𝑧 ∈ On ) → ( 𝑅1 ‘ 𝑧 ) ∈ dom card )
64		r1suc	⊢ ( 𝑧 ∈ On → ( 𝑅1 ‘ suc 𝑧 ) = 𝒫 ( 𝑅1 ‘ 𝑧 ) )
65	64	adantl	⊢ ( ( ∀ 𝑥 ∈ On 𝒫 𝑥 ∈ dom card ∧ 𝑧 ∈ On ) → ( 𝑅1 ‘ suc 𝑧 ) = 𝒫 ( 𝑅1 ‘ 𝑧 ) )
66	65	eleq2d	⊢ ( ( ∀ 𝑥 ∈ On 𝒫 𝑥 ∈ dom card ∧ 𝑧 ∈ On ) → ( 𝑦 ∈ ( 𝑅1 ‘ suc 𝑧 ) ↔ 𝑦 ∈ 𝒫 ( 𝑅1 ‘ 𝑧 ) ) )
67		elpwi	⊢ ( 𝑦 ∈ 𝒫 ( 𝑅1 ‘ 𝑧 ) → 𝑦 ⊆ ( 𝑅1 ‘ 𝑧 ) )
68	66 67	biimtrdi	⊢ ( ( ∀ 𝑥 ∈ On 𝒫 𝑥 ∈ dom card ∧ 𝑧 ∈ On ) → ( 𝑦 ∈ ( 𝑅1 ‘ suc 𝑧 ) → 𝑦 ⊆ ( 𝑅1 ‘ 𝑧 ) ) )
69		ssnum	⊢ ( ( ( 𝑅1 ‘ 𝑧 ) ∈ dom card ∧ 𝑦 ⊆ ( 𝑅1 ‘ 𝑧 ) ) → 𝑦 ∈ dom card )
70	63 68 69	syl6an	⊢ ( ( ∀ 𝑥 ∈ On 𝒫 𝑥 ∈ dom card ∧ 𝑧 ∈ On ) → ( 𝑦 ∈ ( 𝑅1 ‘ suc 𝑧 ) → 𝑦 ∈ dom card ) )
71	70	rexlimdva	⊢ ( ∀ 𝑥 ∈ On 𝒫 𝑥 ∈ dom card → ( ∃ 𝑧 ∈ On 𝑦 ∈ ( 𝑅1 ‘ suc 𝑧 ) → 𝑦 ∈ dom card ) )
72	1 71	biimtrid	⊢ ( ∀ 𝑥 ∈ On 𝒫 𝑥 ∈ dom card → ( 𝑦 ∈ ∪ ( 𝑅1 “ On ) → 𝑦 ∈ dom card ) )
73	72	ssrdv	⊢ ( ∀ 𝑥 ∈ On 𝒫 𝑥 ∈ dom card → ∪ ( 𝑅1 “ On ) ⊆ dom card )
74		onwf	⊢ On ⊆ ∪ ( 𝑅1 “ On )
75	74	sseli	⊢ ( 𝑥 ∈ On → 𝑥 ∈ ∪ ( 𝑅1 “ On ) )
76		pwwf	⊢ ( 𝑥 ∈ ∪ ( 𝑅1 “ On ) ↔ 𝒫 𝑥 ∈ ∪ ( 𝑅1 “ On ) )
77	75 76	sylib	⊢ ( 𝑥 ∈ On → 𝒫 𝑥 ∈ ∪ ( 𝑅1 “ On ) )
78		ssel	⊢ ( ∪ ( 𝑅1 “ On ) ⊆ dom card → ( 𝒫 𝑥 ∈ ∪ ( 𝑅1 “ On ) → 𝒫 𝑥 ∈ dom card ) )
79	77 78	syl5	⊢ ( ∪ ( 𝑅1 “ On ) ⊆ dom card → ( 𝑥 ∈ On → 𝒫 𝑥 ∈ dom card ) )
80	79	ralrimiv	⊢ ( ∪ ( 𝑅1 “ On ) ⊆ dom card → ∀ 𝑥 ∈ On 𝒫 𝑥 ∈ dom card )
81	73 80	impbii	⊢ ( ∀ 𝑥 ∈ On 𝒫 𝑥 ∈ dom card ↔ ∪ ( 𝑅1 “ On ) ⊆ dom card )