Proof of Theorem ttukeylem3
Step | Hyp | Ref
| Expression |
1 | | ttukeylem.4 |
. . . 4
⊢ 𝐺 = recs((𝑧 ∈ V ↦ if(dom 𝑧 = ∪ dom 𝑧, if(dom 𝑧 = ∅, 𝐵, ∪ ran 𝑧), ((𝑧‘∪ dom 𝑧) ∪ if(((𝑧‘∪ dom 𝑧) ∪ {(𝐹‘∪ dom
𝑧)}) ∈ 𝐴, {(𝐹‘∪ dom
𝑧)},
∅))))) |
2 | 1 | tfr2 8034 |
. . 3
⊢ (𝐶 ∈ On → (𝐺‘𝐶) = ((𝑧 ∈ V ↦ if(dom 𝑧 = ∪ dom 𝑧, if(dom 𝑧 = ∅, 𝐵, ∪ ran 𝑧), ((𝑧‘∪ dom 𝑧) ∪ if(((𝑧‘∪ dom 𝑧) ∪ {(𝐹‘∪ dom
𝑧)}) ∈ 𝐴, {(𝐹‘∪ dom
𝑧)},
∅))))‘(𝐺
↾ 𝐶))) |
3 | 2 | adantl 484 |
. 2
⊢ ((𝜑 ∧ 𝐶 ∈ On) → (𝐺‘𝐶) = ((𝑧 ∈ V ↦ if(dom 𝑧 = ∪ dom 𝑧, if(dom 𝑧 = ∅, 𝐵, ∪ ran 𝑧), ((𝑧‘∪ dom 𝑧) ∪ if(((𝑧‘∪ dom 𝑧) ∪ {(𝐹‘∪ dom
𝑧)}) ∈ 𝐴, {(𝐹‘∪ dom
𝑧)},
∅))))‘(𝐺
↾ 𝐶))) |
4 | | eqidd 2822 |
. . 3
⊢ ((𝜑 ∧ 𝐶 ∈ On) → (𝑧 ∈ V ↦ if(dom 𝑧 = ∪ dom 𝑧, if(dom 𝑧 = ∅, 𝐵, ∪ ran 𝑧), ((𝑧‘∪ dom 𝑧) ∪ if(((𝑧‘∪ dom 𝑧) ∪ {(𝐹‘∪ dom
𝑧)}) ∈ 𝐴, {(𝐹‘∪ dom
𝑧)}, ∅)))) = (𝑧 ∈ V ↦ if(dom 𝑧 = ∪
dom 𝑧, if(dom 𝑧 = ∅, 𝐵, ∪ ran 𝑧), ((𝑧‘∪ dom 𝑧) ∪ if(((𝑧‘∪ dom 𝑧) ∪ {(𝐹‘∪ dom
𝑧)}) ∈ 𝐴, {(𝐹‘∪ dom
𝑧)},
∅))))) |
5 | | simpr 487 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → 𝑧 = (𝐺 ↾ 𝐶)) |
6 | 5 | dmeqd 5774 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → dom 𝑧 = dom (𝐺 ↾ 𝐶)) |
7 | 1 | tfr1 8033 |
. . . . . . . . 9
⊢ 𝐺 Fn On |
8 | | onss 7505 |
. . . . . . . . . 10
⊢ (𝐶 ∈ On → 𝐶 ⊆ On) |
9 | 8 | ad2antlr 725 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → 𝐶 ⊆ On) |
10 | | fnssres 6470 |
. . . . . . . . 9
⊢ ((𝐺 Fn On ∧ 𝐶 ⊆ On) → (𝐺 ↾ 𝐶) Fn 𝐶) |
11 | 7, 9, 10 | sylancr 589 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → (𝐺 ↾ 𝐶) Fn 𝐶) |
12 | | fndm 6455 |
. . . . . . . 8
⊢ ((𝐺 ↾ 𝐶) Fn 𝐶 → dom (𝐺 ↾ 𝐶) = 𝐶) |
13 | 11, 12 | syl 17 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → dom (𝐺 ↾ 𝐶) = 𝐶) |
14 | 6, 13 | eqtrd 2856 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → dom 𝑧 = 𝐶) |
15 | 14 | unieqd 4852 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → ∪ dom
𝑧 = ∪ 𝐶) |
16 | 14, 15 | eqeq12d 2837 |
. . . . 5
⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → (dom 𝑧 = ∪ dom 𝑧 ↔ 𝐶 = ∪ 𝐶)) |
17 | 14 | eqeq1d 2823 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → (dom 𝑧 = ∅ ↔ 𝐶 = ∅)) |
18 | 5 | rneqd 5808 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → ran 𝑧 = ran (𝐺 ↾ 𝐶)) |
19 | | df-ima 5568 |
. . . . . . . 8
⊢ (𝐺 “ 𝐶) = ran (𝐺 ↾ 𝐶) |
20 | 18, 19 | syl6eqr 2874 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → ran 𝑧 = (𝐺 “ 𝐶)) |
21 | 20 | unieqd 4852 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → ∪ ran
𝑧 = ∪ (𝐺
“ 𝐶)) |
22 | 17, 21 | ifbieq2d 4492 |
. . . . 5
⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → if(dom 𝑧 = ∅, 𝐵, ∪ ran 𝑧) = if(𝐶 = ∅, 𝐵, ∪ (𝐺 “ 𝐶))) |
23 | 5, 15 | fveq12d 6677 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → (𝑧‘∪ dom 𝑧) = ((𝐺 ↾ 𝐶)‘∪ 𝐶)) |
24 | 15 | fveq2d 6674 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → (𝐹‘∪ dom
𝑧) = (𝐹‘∪ 𝐶)) |
25 | 24 | sneqd 4579 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → {(𝐹‘∪ dom
𝑧)} = {(𝐹‘∪ 𝐶)}) |
26 | 23, 25 | uneq12d 4140 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → ((𝑧‘∪ dom 𝑧) ∪ {(𝐹‘∪ dom
𝑧)}) = (((𝐺 ↾ 𝐶)‘∪ 𝐶) ∪ {(𝐹‘∪ 𝐶)})) |
27 | 26 | eleq1d 2897 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → (((𝑧‘∪ dom 𝑧) ∪ {(𝐹‘∪ dom
𝑧)}) ∈ 𝐴 ↔ (((𝐺 ↾ 𝐶)‘∪ 𝐶) ∪ {(𝐹‘∪ 𝐶)}) ∈ 𝐴)) |
28 | | eqidd 2822 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → ∅ =
∅) |
29 | 27, 25, 28 | ifbieq12d 4494 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → if(((𝑧‘∪ dom 𝑧) ∪ {(𝐹‘∪ dom
𝑧)}) ∈ 𝐴, {(𝐹‘∪ dom
𝑧)}, ∅) = if((((𝐺 ↾ 𝐶)‘∪ 𝐶) ∪ {(𝐹‘∪ 𝐶)}) ∈ 𝐴, {(𝐹‘∪ 𝐶)}, ∅)) |
30 | 23, 29 | uneq12d 4140 |
. . . . 5
⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → ((𝑧‘∪ dom 𝑧) ∪ if(((𝑧‘∪ dom 𝑧) ∪ {(𝐹‘∪ dom
𝑧)}) ∈ 𝐴, {(𝐹‘∪ dom
𝑧)}, ∅)) = (((𝐺 ↾ 𝐶)‘∪ 𝐶) ∪ if((((𝐺 ↾ 𝐶)‘∪ 𝐶) ∪ {(𝐹‘∪ 𝐶)}) ∈ 𝐴, {(𝐹‘∪ 𝐶)}, ∅))) |
31 | 16, 22, 30 | ifbieq12d 4494 |
. . . 4
⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → if(dom 𝑧 = ∪ dom 𝑧, if(dom 𝑧 = ∅, 𝐵, ∪ ran 𝑧), ((𝑧‘∪ dom 𝑧) ∪ if(((𝑧‘∪ dom 𝑧) ∪ {(𝐹‘∪ dom
𝑧)}) ∈ 𝐴, {(𝐹‘∪ dom
𝑧)}, ∅))) = if(𝐶 = ∪
𝐶, if(𝐶 = ∅, 𝐵, ∪ (𝐺 “ 𝐶)), (((𝐺 ↾ 𝐶)‘∪ 𝐶) ∪ if((((𝐺 ↾ 𝐶)‘∪ 𝐶) ∪ {(𝐹‘∪ 𝐶)}) ∈ 𝐴, {(𝐹‘∪ 𝐶)}, ∅)))) |
32 | | onuni 7508 |
. . . . . . . . . 10
⊢ (𝐶 ∈ On → ∪ 𝐶
∈ On) |
33 | 32 | ad3antlr 729 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → ∪ 𝐶
∈ On) |
34 | | sucidg 6269 |
. . . . . . . . 9
⊢ (∪ 𝐶
∈ On → ∪ 𝐶 ∈ suc ∪
𝐶) |
35 | 33, 34 | syl 17 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → ∪ 𝐶
∈ suc ∪ 𝐶) |
36 | | eloni 6201 |
. . . . . . . . . . 11
⊢ (𝐶 ∈ On → Ord 𝐶) |
37 | 36 | ad2antlr 725 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → Ord 𝐶) |
38 | | orduniorsuc 7545 |
. . . . . . . . . 10
⊢ (Ord
𝐶 → (𝐶 = ∪ 𝐶 ∨ 𝐶 = suc ∪ 𝐶)) |
39 | 37, 38 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → (𝐶 = ∪ 𝐶 ∨ 𝐶 = suc ∪ 𝐶)) |
40 | 39 | orcanai 999 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → 𝐶 = suc ∪ 𝐶) |
41 | 35, 40 | eleqtrrd 2916 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → ∪ 𝐶
∈ 𝐶) |
42 | 41 | fvresd 6690 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → ((𝐺 ↾ 𝐶)‘∪ 𝐶) = (𝐺‘∪ 𝐶)) |
43 | 42 | uneq1d 4138 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → (((𝐺 ↾ 𝐶)‘∪ 𝐶) ∪ {(𝐹‘∪ 𝐶)}) = ((𝐺‘∪ 𝐶) ∪ {(𝐹‘∪ 𝐶)})) |
44 | 43 | eleq1d 2897 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → ((((𝐺 ↾ 𝐶)‘∪ 𝐶) ∪ {(𝐹‘∪ 𝐶)}) ∈ 𝐴 ↔ ((𝐺‘∪ 𝐶) ∪ {(𝐹‘∪ 𝐶)}) ∈ 𝐴)) |
45 | 44 | ifbid 4489 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → if((((𝐺 ↾ 𝐶)‘∪ 𝐶) ∪ {(𝐹‘∪ 𝐶)}) ∈ 𝐴, {(𝐹‘∪ 𝐶)}, ∅) = if(((𝐺‘∪ 𝐶)
∪ {(𝐹‘∪ 𝐶)})
∈ 𝐴, {(𝐹‘∪ 𝐶)},
∅)) |
46 | 42, 45 | uneq12d 4140 |
. . . . 5
⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → (((𝐺 ↾ 𝐶)‘∪ 𝐶) ∪ if((((𝐺 ↾ 𝐶)‘∪ 𝐶) ∪ {(𝐹‘∪ 𝐶)}) ∈ 𝐴, {(𝐹‘∪ 𝐶)}, ∅)) = ((𝐺‘∪ 𝐶)
∪ if(((𝐺‘∪ 𝐶)
∪ {(𝐹‘∪ 𝐶)})
∈ 𝐴, {(𝐹‘∪ 𝐶)},
∅))) |
47 | 46 | ifeq2da 4498 |
. . . 4
⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → if(𝐶 = ∪ 𝐶, if(𝐶 = ∅, 𝐵, ∪ (𝐺 “ 𝐶)), (((𝐺 ↾ 𝐶)‘∪ 𝐶) ∪ if((((𝐺 ↾ 𝐶)‘∪ 𝐶) ∪ {(𝐹‘∪ 𝐶)}) ∈ 𝐴, {(𝐹‘∪ 𝐶)}, ∅))) = if(𝐶 = ∪
𝐶, if(𝐶 = ∅, 𝐵, ∪ (𝐺 “ 𝐶)), ((𝐺‘∪ 𝐶) ∪ if(((𝐺‘∪ 𝐶) ∪ {(𝐹‘∪ 𝐶)}) ∈ 𝐴, {(𝐹‘∪ 𝐶)}, ∅)))) |
48 | 31, 47 | eqtrd 2856 |
. . 3
⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → if(dom 𝑧 = ∪ dom 𝑧, if(dom 𝑧 = ∅, 𝐵, ∪ ran 𝑧), ((𝑧‘∪ dom 𝑧) ∪ if(((𝑧‘∪ dom 𝑧) ∪ {(𝐹‘∪ dom
𝑧)}) ∈ 𝐴, {(𝐹‘∪ dom
𝑧)}, ∅))) = if(𝐶 = ∪
𝐶, if(𝐶 = ∅, 𝐵, ∪ (𝐺 “ 𝐶)), ((𝐺‘∪ 𝐶) ∪ if(((𝐺‘∪ 𝐶) ∪ {(𝐹‘∪ 𝐶)}) ∈ 𝐴, {(𝐹‘∪ 𝐶)}, ∅)))) |
49 | | fnfun 6453 |
. . . . 5
⊢ (𝐺 Fn On → Fun 𝐺) |
50 | 7, 49 | ax-mp 5 |
. . . 4
⊢ Fun 𝐺 |
51 | | simpr 487 |
. . . 4
⊢ ((𝜑 ∧ 𝐶 ∈ On) → 𝐶 ∈ On) |
52 | | resfunexg 6978 |
. . . 4
⊢ ((Fun
𝐺 ∧ 𝐶 ∈ On) → (𝐺 ↾ 𝐶) ∈ V) |
53 | 50, 51, 52 | sylancr 589 |
. . 3
⊢ ((𝜑 ∧ 𝐶 ∈ On) → (𝐺 ↾ 𝐶) ∈ V) |
54 | | ttukeylem.2 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ 𝐴) |
55 | 54 | elexd 3514 |
. . . . 5
⊢ (𝜑 → 𝐵 ∈ V) |
56 | | funimaexg 6440 |
. . . . . . 7
⊢ ((Fun
𝐺 ∧ 𝐶 ∈ On) → (𝐺 “ 𝐶) ∈ V) |
57 | 50, 56 | mpan 688 |
. . . . . 6
⊢ (𝐶 ∈ On → (𝐺 “ 𝐶) ∈ V) |
58 | 57 | uniexd 7468 |
. . . . 5
⊢ (𝐶 ∈ On → ∪ (𝐺
“ 𝐶) ∈
V) |
59 | | ifcl 4511 |
. . . . 5
⊢ ((𝐵 ∈ V ∧ ∪ (𝐺
“ 𝐶) ∈ V) →
if(𝐶 = ∅, 𝐵, ∪
(𝐺 “ 𝐶)) ∈ V) |
60 | 55, 58, 59 | syl2an 597 |
. . . 4
⊢ ((𝜑 ∧ 𝐶 ∈ On) → if(𝐶 = ∅, 𝐵, ∪ (𝐺 “ 𝐶)) ∈ V) |
61 | | fvex 6683 |
. . . . 5
⊢ (𝐺‘∪ 𝐶)
∈ V |
62 | | snex 5332 |
. . . . . 6
⊢ {(𝐹‘∪ 𝐶)}
∈ V |
63 | | 0ex 5211 |
. . . . . 6
⊢ ∅
∈ V |
64 | 62, 63 | ifex 4515 |
. . . . 5
⊢
if(((𝐺‘∪ 𝐶)
∪ {(𝐹‘∪ 𝐶)})
∈ 𝐴, {(𝐹‘∪ 𝐶)},
∅) ∈ V |
65 | 61, 64 | unex 7469 |
. . . 4
⊢ ((𝐺‘∪ 𝐶)
∪ if(((𝐺‘∪ 𝐶)
∪ {(𝐹‘∪ 𝐶)})
∈ 𝐴, {(𝐹‘∪ 𝐶)},
∅)) ∈ V |
66 | | ifcl 4511 |
. . . 4
⊢
((if(𝐶 = ∅,
𝐵, ∪ (𝐺
“ 𝐶)) ∈ V ∧
((𝐺‘∪ 𝐶)
∪ if(((𝐺‘∪ 𝐶)
∪ {(𝐹‘∪ 𝐶)})
∈ 𝐴, {(𝐹‘∪ 𝐶)},
∅)) ∈ V) → if(𝐶 = ∪ 𝐶, if(𝐶 = ∅, 𝐵, ∪ (𝐺 “ 𝐶)), ((𝐺‘∪ 𝐶) ∪ if(((𝐺‘∪ 𝐶) ∪ {(𝐹‘∪ 𝐶)}) ∈ 𝐴, {(𝐹‘∪ 𝐶)}, ∅))) ∈
V) |
67 | 60, 65, 66 | sylancl 588 |
. . 3
⊢ ((𝜑 ∧ 𝐶 ∈ On) → if(𝐶 = ∪ 𝐶, if(𝐶 = ∅, 𝐵, ∪ (𝐺 “ 𝐶)), ((𝐺‘∪ 𝐶) ∪ if(((𝐺‘∪ 𝐶) ∪ {(𝐹‘∪ 𝐶)}) ∈ 𝐴, {(𝐹‘∪ 𝐶)}, ∅))) ∈
V) |
68 | 4, 48, 53, 67 | fvmptd 6775 |
. 2
⊢ ((𝜑 ∧ 𝐶 ∈ On) → ((𝑧 ∈ V ↦ if(dom 𝑧 = ∪ dom 𝑧, if(dom 𝑧 = ∅, 𝐵, ∪ ran 𝑧), ((𝑧‘∪ dom 𝑧) ∪ if(((𝑧‘∪ dom 𝑧) ∪ {(𝐹‘∪ dom
𝑧)}) ∈ 𝐴, {(𝐹‘∪ dom
𝑧)},
∅))))‘(𝐺
↾ 𝐶)) = if(𝐶 = ∪
𝐶, if(𝐶 = ∅, 𝐵, ∪ (𝐺 “ 𝐶)), ((𝐺‘∪ 𝐶) ∪ if(((𝐺‘∪ 𝐶) ∪ {(𝐹‘∪ 𝐶)}) ∈ 𝐴, {(𝐹‘∪ 𝐶)}, ∅)))) |
69 | 3, 68 | eqtrd 2856 |
1
⊢ ((𝜑 ∧ 𝐶 ∈ On) → (𝐺‘𝐶) = if(𝐶 = ∪ 𝐶, if(𝐶 = ∅, 𝐵, ∪ (𝐺 “ 𝐶)), ((𝐺‘∪ 𝐶) ∪ if(((𝐺‘∪ 𝐶) ∪ {(𝐹‘∪ 𝐶)}) ∈ 𝐴, {(𝐹‘∪ 𝐶)}, ∅)))) |