MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dfac12r Structured version   Visualization version   GIF version

Theorem dfac12r 10087
Description: The axiom of choice holds iff every ordinal has a well-orderable powerset. This version of dfac12 10090 does not assume the Axiom of Regularity. (Contributed by Mario Carneiro, 29-May-2015.)
Assertion
Ref Expression
dfac12r (βˆ€π‘₯ ∈ On 𝒫 π‘₯ ∈ dom card ↔ βˆͺ (𝑅1 β€œ On) βŠ† dom card)

Proof of Theorem dfac12r
Dummy variables π‘Ž 𝑏 𝑓 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 rankwflemb 9734 . . . 4 (𝑦 ∈ βˆͺ (𝑅1 β€œ On) ↔ βˆƒπ‘§ ∈ On 𝑦 ∈ (𝑅1β€˜suc 𝑧))
2 harcl 9500 . . . . . . . . 9 (harβ€˜(𝑅1β€˜π‘§)) ∈ On
3 pweq 4575 . . . . . . . . . . 11 (π‘₯ = (harβ€˜(𝑅1β€˜π‘§)) β†’ 𝒫 π‘₯ = 𝒫 (harβ€˜(𝑅1β€˜π‘§)))
43eleq1d 2819 . . . . . . . . . 10 (π‘₯ = (harβ€˜(𝑅1β€˜π‘§)) β†’ (𝒫 π‘₯ ∈ dom card ↔ 𝒫 (harβ€˜(𝑅1β€˜π‘§)) ∈ dom card))
54rspcv 3576 . . . . . . . . 9 ((harβ€˜(𝑅1β€˜π‘§)) ∈ On β†’ (βˆ€π‘₯ ∈ On 𝒫 π‘₯ ∈ dom card β†’ 𝒫 (harβ€˜(𝑅1β€˜π‘§)) ∈ dom card))
62, 5ax-mp 5 . . . . . . . 8 (βˆ€π‘₯ ∈ On 𝒫 π‘₯ ∈ dom card β†’ 𝒫 (harβ€˜(𝑅1β€˜π‘§)) ∈ dom card)
7 cardid2 9894 . . . . . . . 8 (𝒫 (harβ€˜(𝑅1β€˜π‘§)) ∈ dom card β†’ (cardβ€˜π’« (harβ€˜(𝑅1β€˜π‘§))) β‰ˆ 𝒫 (harβ€˜(𝑅1β€˜π‘§)))
8 ensym 8946 . . . . . . . 8 ((cardβ€˜π’« (harβ€˜(𝑅1β€˜π‘§))) β‰ˆ 𝒫 (harβ€˜(𝑅1β€˜π‘§)) β†’ 𝒫 (harβ€˜(𝑅1β€˜π‘§)) β‰ˆ (cardβ€˜π’« (harβ€˜(𝑅1β€˜π‘§))))
9 bren 8896 . . . . . . . . 9 (𝒫 (harβ€˜(𝑅1β€˜π‘§)) β‰ˆ (cardβ€˜π’« (harβ€˜(𝑅1β€˜π‘§))) ↔ βˆƒπ‘“ 𝑓:𝒫 (harβ€˜(𝑅1β€˜π‘§))–1-1-ontoβ†’(cardβ€˜π’« (harβ€˜(𝑅1β€˜π‘§))))
10 simpr 486 . . . . . . . . . . . 12 ((𝑓:𝒫 (harβ€˜(𝑅1β€˜π‘§))–1-1-ontoβ†’(cardβ€˜π’« (harβ€˜(𝑅1β€˜π‘§))) ∧ 𝑧 ∈ On) β†’ 𝑧 ∈ On)
11 f1of1 6784 . . . . . . . . . . . . . 14 (𝑓:𝒫 (harβ€˜(𝑅1β€˜π‘§))–1-1-ontoβ†’(cardβ€˜π’« (harβ€˜(𝑅1β€˜π‘§))) β†’ 𝑓:𝒫 (harβ€˜(𝑅1β€˜π‘§))–1-1β†’(cardβ€˜π’« (harβ€˜(𝑅1β€˜π‘§))))
1211adantr 482 . . . . . . . . . . . . 13 ((𝑓:𝒫 (harβ€˜(𝑅1β€˜π‘§))–1-1-ontoβ†’(cardβ€˜π’« (harβ€˜(𝑅1β€˜π‘§))) ∧ 𝑧 ∈ On) β†’ 𝑓:𝒫 (harβ€˜(𝑅1β€˜π‘§))–1-1β†’(cardβ€˜π’« (harβ€˜(𝑅1β€˜π‘§))))
13 cardon 9885 . . . . . . . . . . . . . 14 (cardβ€˜π’« (harβ€˜(𝑅1β€˜π‘§))) ∈ On
1413onssi 7774 . . . . . . . . . . . . 13 (cardβ€˜π’« (harβ€˜(𝑅1β€˜π‘§))) βŠ† On
15 f1ss 6745 . . . . . . . . . . . . 13 ((𝑓:𝒫 (harβ€˜(𝑅1β€˜π‘§))–1-1β†’(cardβ€˜π’« (harβ€˜(𝑅1β€˜π‘§))) ∧ (cardβ€˜π’« (harβ€˜(𝑅1β€˜π‘§))) βŠ† On) β†’ 𝑓:𝒫 (harβ€˜(𝑅1β€˜π‘§))–1-1β†’On)
1612, 14, 15sylancl 587 . . . . . . . . . . . 12 ((𝑓:𝒫 (harβ€˜(𝑅1β€˜π‘§))–1-1-ontoβ†’(cardβ€˜π’« (harβ€˜(𝑅1β€˜π‘§))) ∧ 𝑧 ∈ On) β†’ 𝑓:𝒫 (harβ€˜(𝑅1β€˜π‘§))–1-1β†’On)
17 fveq2 6843 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑏 β†’ (rankβ€˜π‘¦) = (rankβ€˜π‘))
1817oveq2d 7374 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑏 β†’ (suc βˆͺ ran βˆͺ ran π‘₯ Β·o (rankβ€˜π‘¦)) = (suc βˆͺ ran βˆͺ ran π‘₯ Β·o (rankβ€˜π‘)))
19 suceq 6384 . . . . . . . . . . . . . . . . . . . . 21 ((rankβ€˜π‘¦) = (rankβ€˜π‘) β†’ suc (rankβ€˜π‘¦) = suc (rankβ€˜π‘))
2017, 19syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝑏 β†’ suc (rankβ€˜π‘¦) = suc (rankβ€˜π‘))
2120fveq2d 6847 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑏 β†’ (π‘₯β€˜suc (rankβ€˜π‘¦)) = (π‘₯β€˜suc (rankβ€˜π‘)))
22 id 22 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑏 β†’ 𝑦 = 𝑏)
2321, 22fveq12d 6850 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑏 β†’ ((π‘₯β€˜suc (rankβ€˜π‘¦))β€˜π‘¦) = ((π‘₯β€˜suc (rankβ€˜π‘))β€˜π‘))
2418, 23oveq12d 7376 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑏 β†’ ((suc βˆͺ ran βˆͺ ran π‘₯ Β·o (rankβ€˜π‘¦)) +o ((π‘₯β€˜suc (rankβ€˜π‘¦))β€˜π‘¦)) = ((suc βˆͺ ran βˆͺ ran π‘₯ Β·o (rankβ€˜π‘)) +o ((π‘₯β€˜suc (rankβ€˜π‘))β€˜π‘)))
25 imaeq2 6010 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑏 β†’ ((β—‘OrdIso( E , ran (π‘₯β€˜βˆͺ dom π‘₯)) ∘ (π‘₯β€˜βˆͺ dom π‘₯)) β€œ 𝑦) = ((β—‘OrdIso( E , ran (π‘₯β€˜βˆͺ dom π‘₯)) ∘ (π‘₯β€˜βˆͺ dom π‘₯)) β€œ 𝑏))
2625fveq2d 6847 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑏 β†’ (π‘“β€˜((β—‘OrdIso( E , ran (π‘₯β€˜βˆͺ dom π‘₯)) ∘ (π‘₯β€˜βˆͺ dom π‘₯)) β€œ 𝑦)) = (π‘“β€˜((β—‘OrdIso( E , ran (π‘₯β€˜βˆͺ dom π‘₯)) ∘ (π‘₯β€˜βˆͺ dom π‘₯)) β€œ 𝑏)))
2724, 26ifeq12d 4508 . . . . . . . . . . . . . . . 16 (𝑦 = 𝑏 β†’ 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 π‘₯)) β€œ 𝑏))))
2827cbvmptv 5219 . . . . . . . . . . . . . . 15 (𝑦 ∈ (𝑅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 5860 . . . . . . . . . . . . . . . . 17 (π‘₯ = π‘Ž β†’ dom π‘₯ = dom π‘Ž)
3029fveq2d 6847 . . . . . . . . . . . . . . . 16 (π‘₯ = π‘Ž β†’ (𝑅1β€˜dom π‘₯) = (𝑅1β€˜dom π‘Ž))
3129unieqd 4880 . . . . . . . . . . . . . . . . . 18 (π‘₯ = π‘Ž β†’ βˆͺ dom π‘₯ = βˆͺ dom π‘Ž)
3229, 31eqeq12d 2749 . . . . . . . . . . . . . . . . 17 (π‘₯ = π‘Ž β†’ (dom π‘₯ = βˆͺ dom π‘₯ ↔ dom π‘Ž = βˆͺ dom π‘Ž))
33 rneq 5892 . . . . . . . . . . . . . . . . . . . . . . 23 (π‘₯ = π‘Ž β†’ ran π‘₯ = ran π‘Ž)
3433unieqd 4880 . . . . . . . . . . . . . . . . . . . . . 22 (π‘₯ = π‘Ž β†’ βˆͺ ran π‘₯ = βˆͺ ran π‘Ž)
3534rneqd 5894 . . . . . . . . . . . . . . . . . . . . 21 (π‘₯ = π‘Ž β†’ ran βˆͺ ran π‘₯ = ran βˆͺ ran π‘Ž)
3635unieqd 4880 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ = π‘Ž β†’ βˆͺ ran βˆͺ ran π‘₯ = βˆͺ ran βˆͺ ran π‘Ž)
37 suceq 6384 . . . . . . . . . . . . . . . . . . . 20 (βˆͺ ran βˆͺ ran π‘₯ = βˆͺ ran βˆͺ ran π‘Ž β†’ suc βˆͺ ran βˆͺ ran π‘₯ = suc βˆͺ ran βˆͺ ran π‘Ž)
3836, 37syl 17 . . . . . . . . . . . . . . . . . . 19 (π‘₯ = π‘Ž β†’ suc βˆͺ ran βˆͺ ran π‘₯ = suc βˆͺ ran βˆͺ ran π‘Ž)
3938oveq1d 7373 . . . . . . . . . . . . . . . . . 18 (π‘₯ = π‘Ž β†’ (suc βˆͺ ran βˆͺ ran π‘₯ Β·o (rankβ€˜π‘)) = (suc βˆͺ ran βˆͺ ran π‘Ž Β·o (rankβ€˜π‘)))
40 fveq1 6842 . . . . . . . . . . . . . . . . . . 19 (π‘₯ = π‘Ž β†’ (π‘₯β€˜suc (rankβ€˜π‘)) = (π‘Žβ€˜suc (rankβ€˜π‘)))
4140fveq1d 6845 . . . . . . . . . . . . . . . . . 18 (π‘₯ = π‘Ž β†’ ((π‘₯β€˜suc (rankβ€˜π‘))β€˜π‘) = ((π‘Žβ€˜suc (rankβ€˜π‘))β€˜π‘))
4239, 41oveq12d 7376 . . . . . . . . . . . . . . . . 17 (π‘₯ = π‘Ž β†’ ((suc βˆͺ ran βˆͺ ran π‘₯ Β·o (rankβ€˜π‘)) +o ((π‘₯β€˜suc (rankβ€˜π‘))β€˜π‘)) = ((suc βˆͺ ran βˆͺ ran π‘Ž Β·o (rankβ€˜π‘)) +o ((π‘Žβ€˜suc (rankβ€˜π‘))β€˜π‘)))
43 id 22 . . . . . . . . . . . . . . . . . . . . . . . 24 (π‘₯ = π‘Ž β†’ π‘₯ = π‘Ž)
4443, 31fveq12d 6850 . . . . . . . . . . . . . . . . . . . . . . 23 (π‘₯ = π‘Ž β†’ (π‘₯β€˜βˆͺ dom π‘₯) = (π‘Žβ€˜βˆͺ dom π‘Ž))
4544rneqd 5894 . . . . . . . . . . . . . . . . . . . . . 22 (π‘₯ = π‘Ž β†’ ran (π‘₯β€˜βˆͺ dom π‘₯) = ran (π‘Žβ€˜βˆͺ dom π‘Ž))
46 oieq2 9454 . . . . . . . . . . . . . . . . . . . . . 22 (ran (π‘₯β€˜βˆͺ dom π‘₯) = ran (π‘Žβ€˜βˆͺ dom π‘Ž) β†’ OrdIso( E , ran (π‘₯β€˜βˆͺ dom π‘₯)) = OrdIso( E , ran (π‘Žβ€˜βˆͺ dom π‘Ž)))
4745, 46syl 17 . . . . . . . . . . . . . . . . . . . . 21 (π‘₯ = π‘Ž β†’ OrdIso( E , ran (π‘₯β€˜βˆͺ dom π‘₯)) = OrdIso( E , ran (π‘Žβ€˜βˆͺ dom π‘Ž)))
4847cnveqd 5832 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ = π‘Ž β†’ β—‘OrdIso( E , ran (π‘₯β€˜βˆͺ dom π‘₯)) = β—‘OrdIso( E , ran (π‘Žβ€˜βˆͺ dom π‘Ž)))
4948, 44coeq12d 5821 . . . . . . . . . . . . . . . . . . 19 (π‘₯ = π‘Ž β†’ (β—‘OrdIso( E , ran (π‘₯β€˜βˆͺ dom π‘₯)) ∘ (π‘₯β€˜βˆͺ dom π‘₯)) = (β—‘OrdIso( E , ran (π‘Žβ€˜βˆͺ dom π‘Ž)) ∘ (π‘Žβ€˜βˆͺ dom π‘Ž)))
5049imaeq1d 6013 . . . . . . . . . . . . . . . . . 18 (π‘₯ = π‘Ž β†’ ((β—‘OrdIso( E , ran (π‘₯β€˜βˆͺ dom π‘₯)) ∘ (π‘₯β€˜βˆͺ dom π‘₯)) β€œ 𝑏) = ((β—‘OrdIso( E , ran (π‘Žβ€˜βˆͺ dom π‘Ž)) ∘ (π‘Žβ€˜βˆͺ dom π‘Ž)) β€œ 𝑏))
5150fveq2d 6847 . . . . . . . . . . . . . . . . 17 (π‘₯ = π‘Ž β†’ (π‘“β€˜((β—‘OrdIso( E , ran (π‘₯β€˜βˆͺ dom π‘₯)) ∘ (π‘₯β€˜βˆͺ dom π‘₯)) β€œ 𝑏)) = (π‘“β€˜((β—‘OrdIso( E , ran (π‘Žβ€˜βˆͺ dom π‘Ž)) ∘ (π‘Žβ€˜βˆͺ dom π‘Ž)) β€œ 𝑏)))
5232, 42, 51ifbieq12d 4515 . . . . . . . . . . . . . . . 16 (π‘₯ = π‘Ž β†’ 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 π‘Ž)) β€œ 𝑏))))
5330, 52mpteq12dv 5197 . . . . . . . . . . . . . . 15 (π‘₯ = π‘Ž β†’ (𝑏 ∈ (𝑅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 π‘Ž)) β€œ 𝑏)))))
5428, 53eqtrid 2785 . . . . . . . . . . . . . 14 (π‘₯ = π‘Ž β†’ (𝑦 ∈ (𝑅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 π‘Ž)) β€œ 𝑏)))))
5554cbvmptv 5219 . . . . . . . . . . . . 13 (π‘₯ ∈ 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 8321 . . . . . . . . . . . . 13 ((π‘₯ ∈ 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 π‘Ž)) β€œ 𝑏)))))))
5755, 56ax-mp 5 . . . . . . . . . . . 12 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 π‘Ž)) β€œ 𝑏))))))
5810, 16, 57dfac12lem3 10086 . . . . . . . . . . 11 ((𝑓:𝒫 (harβ€˜(𝑅1β€˜π‘§))–1-1-ontoβ†’(cardβ€˜π’« (harβ€˜(𝑅1β€˜π‘§))) ∧ 𝑧 ∈ On) β†’ (𝑅1β€˜π‘§) ∈ dom card)
5958ex 414 . . . . . . . . . 10 (𝑓:𝒫 (harβ€˜(𝑅1β€˜π‘§))–1-1-ontoβ†’(cardβ€˜π’« (harβ€˜(𝑅1β€˜π‘§))) β†’ (𝑧 ∈ On β†’ (𝑅1β€˜π‘§) ∈ dom card))
6059exlimiv 1934 . . . . . . . . 9 (βˆƒπ‘“ 𝑓:𝒫 (harβ€˜(𝑅1β€˜π‘§))–1-1-ontoβ†’(cardβ€˜π’« (harβ€˜(𝑅1β€˜π‘§))) β†’ (𝑧 ∈ On β†’ (𝑅1β€˜π‘§) ∈ dom card))
619, 60sylbi 216 . . . . . . . 8 (𝒫 (harβ€˜(𝑅1β€˜π‘§)) β‰ˆ (cardβ€˜π’« (harβ€˜(𝑅1β€˜π‘§))) β†’ (𝑧 ∈ On β†’ (𝑅1β€˜π‘§) ∈ dom card))
626, 7, 8, 614syl 19 . . . . . . 7 (βˆ€π‘₯ ∈ On 𝒫 π‘₯ ∈ dom card β†’ (𝑧 ∈ On β†’ (𝑅1β€˜π‘§) ∈ dom card))
6362imp 408 . . . . . 6 ((βˆ€π‘₯ ∈ On 𝒫 π‘₯ ∈ dom card ∧ 𝑧 ∈ On) β†’ (𝑅1β€˜π‘§) ∈ dom card)
64 r1suc 9711 . . . . . . . . 9 (𝑧 ∈ On β†’ (𝑅1β€˜suc 𝑧) = 𝒫 (𝑅1β€˜π‘§))
6564adantl 483 . . . . . . . 8 ((βˆ€π‘₯ ∈ On 𝒫 π‘₯ ∈ dom card ∧ 𝑧 ∈ On) β†’ (𝑅1β€˜suc 𝑧) = 𝒫 (𝑅1β€˜π‘§))
6665eleq2d 2820 . . . . . . 7 ((βˆ€π‘₯ ∈ On 𝒫 π‘₯ ∈ dom card ∧ 𝑧 ∈ On) β†’ (𝑦 ∈ (𝑅1β€˜suc 𝑧) ↔ 𝑦 ∈ 𝒫 (𝑅1β€˜π‘§)))
67 elpwi 4568 . . . . . . 7 (𝑦 ∈ 𝒫 (𝑅1β€˜π‘§) β†’ 𝑦 βŠ† (𝑅1β€˜π‘§))
6866, 67syl6bi 253 . . . . . 6 ((βˆ€π‘₯ ∈ On 𝒫 π‘₯ ∈ dom card ∧ 𝑧 ∈ On) β†’ (𝑦 ∈ (𝑅1β€˜suc 𝑧) β†’ 𝑦 βŠ† (𝑅1β€˜π‘§)))
69 ssnum 9980 . . . . . 6 (((𝑅1β€˜π‘§) ∈ dom card ∧ 𝑦 βŠ† (𝑅1β€˜π‘§)) β†’ 𝑦 ∈ dom card)
7063, 68, 69syl6an 683 . . . . 5 ((βˆ€π‘₯ ∈ On 𝒫 π‘₯ ∈ dom card ∧ 𝑧 ∈ On) β†’ (𝑦 ∈ (𝑅1β€˜suc 𝑧) β†’ 𝑦 ∈ dom card))
7170rexlimdva 3149 . . . 4 (βˆ€π‘₯ ∈ On 𝒫 π‘₯ ∈ dom card β†’ (βˆƒπ‘§ ∈ On 𝑦 ∈ (𝑅1β€˜suc 𝑧) β†’ 𝑦 ∈ dom card))
721, 71biimtrid 241 . . 3 (βˆ€π‘₯ ∈ On 𝒫 π‘₯ ∈ dom card β†’ (𝑦 ∈ βˆͺ (𝑅1 β€œ On) β†’ 𝑦 ∈ dom card))
7372ssrdv 3951 . 2 (βˆ€π‘₯ ∈ On 𝒫 π‘₯ ∈ dom card β†’ βˆͺ (𝑅1 β€œ On) βŠ† dom card)
74 onwf 9771 . . . . . 6 On βŠ† βˆͺ (𝑅1 β€œ On)
7574sseli 3941 . . . . 5 (π‘₯ ∈ On β†’ π‘₯ ∈ βˆͺ (𝑅1 β€œ On))
76 pwwf 9748 . . . . 5 (π‘₯ ∈ βˆͺ (𝑅1 β€œ On) ↔ 𝒫 π‘₯ ∈ βˆͺ (𝑅1 β€œ On))
7775, 76sylib 217 . . . 4 (π‘₯ ∈ On β†’ 𝒫 π‘₯ ∈ βˆͺ (𝑅1 β€œ On))
78 ssel 3938 . . . 4 (βˆͺ (𝑅1 β€œ On) βŠ† dom card β†’ (𝒫 π‘₯ ∈ βˆͺ (𝑅1 β€œ On) β†’ 𝒫 π‘₯ ∈ dom card))
7977, 78syl5 34 . . 3 (βˆͺ (𝑅1 β€œ On) βŠ† dom card β†’ (π‘₯ ∈ On β†’ 𝒫 π‘₯ ∈ dom card))
8079ralrimiv 3139 . 2 (βˆͺ (𝑅1 β€œ On) βŠ† dom card β†’ βˆ€π‘₯ ∈ On 𝒫 π‘₯ ∈ dom card)
8173, 80impbii 208 1 (βˆ€π‘₯ ∈ On 𝒫 π‘₯ ∈ dom card ↔ βˆͺ (𝑅1 β€œ On) βŠ† dom card)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542  βˆƒwex 1782   ∈ wcel 2107  βˆ€wral 3061  βˆƒwrex 3070  Vcvv 3444   βŠ† wss 3911  ifcif 4487  π’« cpw 4561  βˆͺ cuni 4866   class class class wbr 5106   ↦ cmpt 5189   E cep 5537  β—‘ccnv 5633  dom cdm 5634  ran crn 5635   β€œ cima 5637   ∘ ccom 5638  Oncon0 6318  suc csuc 6320  β€“1-1β†’wf1 6494  β€“1-1-ontoβ†’wf1o 6496  β€˜cfv 6497  (class class class)co 7358  recscrecs 8317   +o coa 8410   Β·o comu 8411   β‰ˆ cen 8883  OrdIsocoi 9450  harchar 9497  π‘…1cr1 9703  rankcrnk 9704  cardccrd 9876
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5243  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3352  df-reu 3353  df-rab 3407  df-v 3446  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3930  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-int 4909  df-iun 4957  df-br 5107  df-opab 5169  df-mpt 5190  df-tr 5224  df-id 5532  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5589  df-se 5590  df-we 5591  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-pred 6254  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505  df-isom 6506  df-riota 7314  df-ov 7361  df-oprab 7362  df-mpo 7363  df-om 7804  df-2nd 7923  df-frecs 8213  df-wrecs 8244  df-recs 8318  df-rdg 8357  df-oadd 8417  df-omul 8418  df-er 8651  df-en 8887  df-dom 8888  df-oi 9451  df-har 9498  df-r1 9705  df-rank 9706  df-card 9880
This theorem is referenced by:  dfac12a  10089
  Copyright terms: Public domain W3C validator