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 7494 |
. . 3
⊢ (𝐶 ∈ On → (𝐺‘𝐶) = ((𝑧 ∈ V ↦ if(dom 𝑧 = ∪ dom 𝑧, if(dom 𝑧 = ∅, 𝐵, ∪ ran 𝑧), ((𝑧‘∪ dom 𝑧) ∪ if(((𝑧‘∪ dom 𝑧) ∪ {(𝐹‘∪ dom
𝑧)}) ∈ 𝐴, {(𝐹‘∪ dom
𝑧)},
∅))))‘(𝐺
↾ 𝐶))) |
3 | 2 | adantl 482 |
. 2
⊢ ((𝜑 ∧ 𝐶 ∈ On) → (𝐺‘𝐶) = ((𝑧 ∈ V ↦ if(dom 𝑧 = ∪ dom 𝑧, if(dom 𝑧 = ∅, 𝐵, ∪ ran 𝑧), ((𝑧‘∪ dom 𝑧) ∪ if(((𝑧‘∪ dom 𝑧) ∪ {(𝐹‘∪ dom
𝑧)}) ∈ 𝐴, {(𝐹‘∪ dom
𝑧)},
∅))))‘(𝐺
↾ 𝐶))) |
4 | | eqidd 2623 |
. . 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 477 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → 𝑧 = (𝐺 ↾ 𝐶)) |
6 | 5 | dmeqd 5326 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → dom 𝑧 = dom (𝐺 ↾ 𝐶)) |
7 | 1 | tfr1 7493 |
. . . . . . . . 9
⊢ 𝐺 Fn On |
8 | | onss 6990 |
. . . . . . . . . 10
⊢ (𝐶 ∈ On → 𝐶 ⊆ On) |
9 | 8 | ad2antlr 763 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → 𝐶 ⊆ On) |
10 | | fnssres 6004 |
. . . . . . . . 9
⊢ ((𝐺 Fn On ∧ 𝐶 ⊆ On) → (𝐺 ↾ 𝐶) Fn 𝐶) |
11 | 7, 9, 10 | sylancr 695 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → (𝐺 ↾ 𝐶) Fn 𝐶) |
12 | | fndm 5990 |
. . . . . . . 8
⊢ ((𝐺 ↾ 𝐶) Fn 𝐶 → dom (𝐺 ↾ 𝐶) = 𝐶) |
13 | 11, 12 | syl 17 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → dom (𝐺 ↾ 𝐶) = 𝐶) |
14 | 6, 13 | eqtrd 2656 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → dom 𝑧 = 𝐶) |
15 | 14 | unieqd 4446 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → ∪ dom
𝑧 = ∪ 𝐶) |
16 | 14, 15 | eqeq12d 2637 |
. . . . 5
⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → (dom 𝑧 = ∪ dom 𝑧 ↔ 𝐶 = ∪ 𝐶)) |
17 | 14 | eqeq1d 2624 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → (dom 𝑧 = ∅ ↔ 𝐶 = ∅)) |
18 | 5 | rneqd 5353 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → ran 𝑧 = ran (𝐺 ↾ 𝐶)) |
19 | | df-ima 5127 |
. . . . . . . 8
⊢ (𝐺 “ 𝐶) = ran (𝐺 ↾ 𝐶) |
20 | 18, 19 | syl6eqr 2674 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → ran 𝑧 = (𝐺 “ 𝐶)) |
21 | 20 | unieqd 4446 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → ∪ ran
𝑧 = ∪ (𝐺
“ 𝐶)) |
22 | 17, 21 | ifbieq2d 4111 |
. . . . 5
⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → if(dom 𝑧 = ∅, 𝐵, ∪ ran 𝑧) = if(𝐶 = ∅, 𝐵, ∪ (𝐺 “ 𝐶))) |
23 | 5, 15 | fveq12d 6197 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → (𝑧‘∪ dom 𝑧) = ((𝐺 ↾ 𝐶)‘∪ 𝐶)) |
24 | 15 | fveq2d 6195 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → (𝐹‘∪ dom
𝑧) = (𝐹‘∪ 𝐶)) |
25 | 24 | sneqd 4189 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → {(𝐹‘∪ dom
𝑧)} = {(𝐹‘∪ 𝐶)}) |
26 | 23, 25 | uneq12d 3768 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → ((𝑧‘∪ dom 𝑧) ∪ {(𝐹‘∪ dom
𝑧)}) = (((𝐺 ↾ 𝐶)‘∪ 𝐶) ∪ {(𝐹‘∪ 𝐶)})) |
27 | 26 | eleq1d 2686 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → (((𝑧‘∪ dom 𝑧) ∪ {(𝐹‘∪ dom
𝑧)}) ∈ 𝐴 ↔ (((𝐺 ↾ 𝐶)‘∪ 𝐶) ∪ {(𝐹‘∪ 𝐶)}) ∈ 𝐴)) |
28 | | eqidd 2623 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → ∅ =
∅) |
29 | 27, 25, 28 | ifbieq12d 4113 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → if(((𝑧‘∪ dom 𝑧) ∪ {(𝐹‘∪ dom
𝑧)}) ∈ 𝐴, {(𝐹‘∪ dom
𝑧)}, ∅) = if((((𝐺 ↾ 𝐶)‘∪ 𝐶) ∪ {(𝐹‘∪ 𝐶)}) ∈ 𝐴, {(𝐹‘∪ 𝐶)}, ∅)) |
30 | 23, 29 | uneq12d 3768 |
. . . . 5
⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → ((𝑧‘∪ dom 𝑧) ∪ if(((𝑧‘∪ dom 𝑧) ∪ {(𝐹‘∪ dom
𝑧)}) ∈ 𝐴, {(𝐹‘∪ dom
𝑧)}, ∅)) = (((𝐺 ↾ 𝐶)‘∪ 𝐶) ∪ if((((𝐺 ↾ 𝐶)‘∪ 𝐶) ∪ {(𝐹‘∪ 𝐶)}) ∈ 𝐴, {(𝐹‘∪ 𝐶)}, ∅))) |
31 | 16, 22, 30 | ifbieq12d 4113 |
. . . 4
⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → if(dom 𝑧 = ∪ dom 𝑧, if(dom 𝑧 = ∅, 𝐵, ∪ ran 𝑧), ((𝑧‘∪ dom 𝑧) ∪ if(((𝑧‘∪ dom 𝑧) ∪ {(𝐹‘∪ dom
𝑧)}) ∈ 𝐴, {(𝐹‘∪ dom
𝑧)}, ∅))) = if(𝐶 = ∪
𝐶, if(𝐶 = ∅, 𝐵, ∪ (𝐺 “ 𝐶)), (((𝐺 ↾ 𝐶)‘∪ 𝐶) ∪ if((((𝐺 ↾ 𝐶)‘∪ 𝐶) ∪ {(𝐹‘∪ 𝐶)}) ∈ 𝐴, {(𝐹‘∪ 𝐶)}, ∅)))) |
32 | | onuni 6993 |
. . . . . . . . . 10
⊢ (𝐶 ∈ On → ∪ 𝐶
∈ On) |
33 | 32 | ad3antlr 767 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → ∪ 𝐶
∈ On) |
34 | | sucidg 5803 |
. . . . . . . . 9
⊢ (∪ 𝐶
∈ On → ∪ 𝐶 ∈ suc ∪
𝐶) |
35 | 33, 34 | syl 17 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → ∪ 𝐶
∈ suc ∪ 𝐶) |
36 | | eloni 5733 |
. . . . . . . . . . 11
⊢ (𝐶 ∈ On → Ord 𝐶) |
37 | 36 | ad2antlr 763 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → Ord 𝐶) |
38 | | orduniorsuc 7030 |
. . . . . . . . . 10
⊢ (Ord
𝐶 → (𝐶 = ∪ 𝐶 ∨ 𝐶 = suc ∪ 𝐶)) |
39 | 37, 38 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → (𝐶 = ∪ 𝐶 ∨ 𝐶 = suc ∪ 𝐶)) |
40 | 39 | orcanai 952 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → 𝐶 = suc ∪ 𝐶) |
41 | 35, 40 | eleqtrrd 2704 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → ∪ 𝐶
∈ 𝐶) |
42 | | fvres 6207 |
. . . . . . 7
⊢ (∪ 𝐶
∈ 𝐶 → ((𝐺 ↾ 𝐶)‘∪ 𝐶) = (𝐺‘∪ 𝐶)) |
43 | 41, 42 | syl 17 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → ((𝐺 ↾ 𝐶)‘∪ 𝐶) = (𝐺‘∪ 𝐶)) |
44 | 43 | uneq1d 3766 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → (((𝐺 ↾ 𝐶)‘∪ 𝐶) ∪ {(𝐹‘∪ 𝐶)}) = ((𝐺‘∪ 𝐶) ∪ {(𝐹‘∪ 𝐶)})) |
45 | 44 | eleq1d 2686 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → ((((𝐺 ↾ 𝐶)‘∪ 𝐶) ∪ {(𝐹‘∪ 𝐶)}) ∈ 𝐴 ↔ ((𝐺‘∪ 𝐶) ∪ {(𝐹‘∪ 𝐶)}) ∈ 𝐴)) |
46 | 45 | ifbid 4108 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → if((((𝐺 ↾ 𝐶)‘∪ 𝐶) ∪ {(𝐹‘∪ 𝐶)}) ∈ 𝐴, {(𝐹‘∪ 𝐶)}, ∅) = if(((𝐺‘∪ 𝐶)
∪ {(𝐹‘∪ 𝐶)})
∈ 𝐴, {(𝐹‘∪ 𝐶)},
∅)) |
47 | 43, 46 | uneq12d 3768 |
. . . . 5
⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → (((𝐺 ↾ 𝐶)‘∪ 𝐶) ∪ if((((𝐺 ↾ 𝐶)‘∪ 𝐶) ∪ {(𝐹‘∪ 𝐶)}) ∈ 𝐴, {(𝐹‘∪ 𝐶)}, ∅)) = ((𝐺‘∪ 𝐶)
∪ if(((𝐺‘∪ 𝐶)
∪ {(𝐹‘∪ 𝐶)})
∈ 𝐴, {(𝐹‘∪ 𝐶)},
∅))) |
48 | 47 | ifeq2da 4117 |
. . . 4
⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → if(𝐶 = ∪ 𝐶, if(𝐶 = ∅, 𝐵, ∪ (𝐺 “ 𝐶)), (((𝐺 ↾ 𝐶)‘∪ 𝐶) ∪ if((((𝐺 ↾ 𝐶)‘∪ 𝐶) ∪ {(𝐹‘∪ 𝐶)}) ∈ 𝐴, {(𝐹‘∪ 𝐶)}, ∅))) = if(𝐶 = ∪
𝐶, if(𝐶 = ∅, 𝐵, ∪ (𝐺 “ 𝐶)), ((𝐺‘∪ 𝐶) ∪ if(((𝐺‘∪ 𝐶) ∪ {(𝐹‘∪ 𝐶)}) ∈ 𝐴, {(𝐹‘∪ 𝐶)}, ∅)))) |
49 | 31, 48 | eqtrd 2656 |
. . 3
⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → if(dom 𝑧 = ∪ dom 𝑧, if(dom 𝑧 = ∅, 𝐵, ∪ ran 𝑧), ((𝑧‘∪ dom 𝑧) ∪ if(((𝑧‘∪ dom 𝑧) ∪ {(𝐹‘∪ dom
𝑧)}) ∈ 𝐴, {(𝐹‘∪ dom
𝑧)}, ∅))) = if(𝐶 = ∪
𝐶, if(𝐶 = ∅, 𝐵, ∪ (𝐺 “ 𝐶)), ((𝐺‘∪ 𝐶) ∪ if(((𝐺‘∪ 𝐶) ∪ {(𝐹‘∪ 𝐶)}) ∈ 𝐴, {(𝐹‘∪ 𝐶)}, ∅)))) |
50 | | fnfun 5988 |
. . . . 5
⊢ (𝐺 Fn On → Fun 𝐺) |
51 | 7, 50 | ax-mp 5 |
. . . 4
⊢ Fun 𝐺 |
52 | | simpr 477 |
. . . 4
⊢ ((𝜑 ∧ 𝐶 ∈ On) → 𝐶 ∈ On) |
53 | | resfunexg 6479 |
. . . 4
⊢ ((Fun
𝐺 ∧ 𝐶 ∈ On) → (𝐺 ↾ 𝐶) ∈ V) |
54 | 51, 52, 53 | sylancr 695 |
. . 3
⊢ ((𝜑 ∧ 𝐶 ∈ On) → (𝐺 ↾ 𝐶) ∈ V) |
55 | | ttukeylem.2 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ 𝐴) |
56 | | elex 3212 |
. . . . . 6
⊢ (𝐵 ∈ 𝐴 → 𝐵 ∈ V) |
57 | 55, 56 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐵 ∈ V) |
58 | | funimaexg 5975 |
. . . . . . 7
⊢ ((Fun
𝐺 ∧ 𝐶 ∈ On) → (𝐺 “ 𝐶) ∈ V) |
59 | 51, 58 | mpan 706 |
. . . . . 6
⊢ (𝐶 ∈ On → (𝐺 “ 𝐶) ∈ V) |
60 | | uniexg 6955 |
. . . . . 6
⊢ ((𝐺 “ 𝐶) ∈ V → ∪ (𝐺
“ 𝐶) ∈
V) |
61 | 59, 60 | syl 17 |
. . . . 5
⊢ (𝐶 ∈ On → ∪ (𝐺
“ 𝐶) ∈
V) |
62 | | ifcl 4130 |
. . . . 5
⊢ ((𝐵 ∈ V ∧ ∪ (𝐺
“ 𝐶) ∈ V) →
if(𝐶 = ∅, 𝐵, ∪
(𝐺 “ 𝐶)) ∈ V) |
63 | 57, 61, 62 | syl2an 494 |
. . . 4
⊢ ((𝜑 ∧ 𝐶 ∈ On) → if(𝐶 = ∅, 𝐵, ∪ (𝐺 “ 𝐶)) ∈ V) |
64 | | fvex 6201 |
. . . . 5
⊢ (𝐺‘∪ 𝐶)
∈ V |
65 | | snex 4908 |
. . . . . 6
⊢ {(𝐹‘∪ 𝐶)}
∈ V |
66 | | 0ex 4790 |
. . . . . 6
⊢ ∅
∈ V |
67 | 65, 66 | ifex 4156 |
. . . . 5
⊢
if(((𝐺‘∪ 𝐶)
∪ {(𝐹‘∪ 𝐶)})
∈ 𝐴, {(𝐹‘∪ 𝐶)},
∅) ∈ V |
68 | 64, 67 | unex 6956 |
. . . 4
⊢ ((𝐺‘∪ 𝐶)
∪ if(((𝐺‘∪ 𝐶)
∪ {(𝐹‘∪ 𝐶)})
∈ 𝐴, {(𝐹‘∪ 𝐶)},
∅)) ∈ V |
69 | | ifcl 4130 |
. . . 4
⊢
((if(𝐶 = ∅,
𝐵, ∪ (𝐺
“ 𝐶)) ∈ V ∧
((𝐺‘∪ 𝐶)
∪ if(((𝐺‘∪ 𝐶)
∪ {(𝐹‘∪ 𝐶)})
∈ 𝐴, {(𝐹‘∪ 𝐶)},
∅)) ∈ V) → if(𝐶 = ∪ 𝐶, if(𝐶 = ∅, 𝐵, ∪ (𝐺 “ 𝐶)), ((𝐺‘∪ 𝐶) ∪ if(((𝐺‘∪ 𝐶) ∪ {(𝐹‘∪ 𝐶)}) ∈ 𝐴, {(𝐹‘∪ 𝐶)}, ∅))) ∈
V) |
70 | 63, 68, 69 | sylancl 694 |
. . 3
⊢ ((𝜑 ∧ 𝐶 ∈ On) → if(𝐶 = ∪ 𝐶, if(𝐶 = ∅, 𝐵, ∪ (𝐺 “ 𝐶)), ((𝐺‘∪ 𝐶) ∪ if(((𝐺‘∪ 𝐶) ∪ {(𝐹‘∪ 𝐶)}) ∈ 𝐴, {(𝐹‘∪ 𝐶)}, ∅))) ∈
V) |
71 | 4, 49, 54, 70 | fvmptd 6288 |
. 2
⊢ ((𝜑 ∧ 𝐶 ∈ On) → ((𝑧 ∈ V ↦ if(dom 𝑧 = ∪ dom 𝑧, if(dom 𝑧 = ∅, 𝐵, ∪ ran 𝑧), ((𝑧‘∪ dom 𝑧) ∪ if(((𝑧‘∪ dom 𝑧) ∪ {(𝐹‘∪ dom
𝑧)}) ∈ 𝐴, {(𝐹‘∪ dom
𝑧)},
∅))))‘(𝐺
↾ 𝐶)) = if(𝐶 = ∪
𝐶, if(𝐶 = ∅, 𝐵, ∪ (𝐺 “ 𝐶)), ((𝐺‘∪ 𝐶) ∪ if(((𝐺‘∪ 𝐶) ∪ {(𝐹‘∪ 𝐶)}) ∈ 𝐴, {(𝐹‘∪ 𝐶)}, ∅)))) |
72 | 3, 71 | eqtrd 2656 |
1
⊢ ((𝜑 ∧ 𝐶 ∈ On) → (𝐺‘𝐶) = if(𝐶 = ∪ 𝐶, if(𝐶 = ∅, 𝐵, ∪ (𝐺 “ 𝐶)), ((𝐺‘∪ 𝐶) ∪ if(((𝐺‘∪ 𝐶) ∪ {(𝐹‘∪ 𝐶)}) ∈ 𝐴, {(𝐹‘∪ 𝐶)}, ∅)))) |