Metamath Proof Explorer

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 syl5eq ⊢ ( 𝑥 = 𝑎 → ( 𝑦 ∈ ( 𝑅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 syl6bi ⊢ ( ( ∀ 𝑥 ∈ 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 syl5bi ⊢ ( ∀ 𝑥 ∈ 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 )