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 8438 | . . 3
⊢ (𝐶 ∈ On → (𝐺‘𝐶) = ((𝑧 ∈ V ↦ if(dom 𝑧 = ∪ dom 𝑧, if(dom 𝑧 = ∅, 𝐵, ∪ ran 𝑧), ((𝑧‘∪ dom 𝑧) ∪ if(((𝑧‘∪ dom 𝑧) ∪ {(𝐹‘∪ dom
𝑧)}) ∈ 𝐴, {(𝐹‘∪ dom
𝑧)},
∅))))‘(𝐺
↾ 𝐶))) | 
| 3 | 2 | adantl 481 | . 2
⊢ ((𝜑 ∧ 𝐶 ∈ On) → (𝐺‘𝐶) = ((𝑧 ∈ V ↦ if(dom 𝑧 = ∪ dom 𝑧, if(dom 𝑧 = ∅, 𝐵, ∪ ran 𝑧), ((𝑧‘∪ dom 𝑧) ∪ if(((𝑧‘∪ dom 𝑧) ∪ {(𝐹‘∪ dom
𝑧)}) ∈ 𝐴, {(𝐹‘∪ dom
𝑧)},
∅))))‘(𝐺
↾ 𝐶))) | 
| 4 |  | eqidd 2738 | . . 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 484 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → 𝑧 = (𝐺 ↾ 𝐶)) | 
| 6 | 5 | dmeqd 5916 | . . . . . . 7
⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → dom 𝑧 = dom (𝐺 ↾ 𝐶)) | 
| 7 | 1 | tfr1 8437 | . . . . . . . . 9
⊢ 𝐺 Fn On | 
| 8 |  | onss 7805 | . . . . . . . . . 10
⊢ (𝐶 ∈ On → 𝐶 ⊆ On) | 
| 9 | 8 | ad2antlr 727 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → 𝐶 ⊆ On) | 
| 10 |  | fnssres 6691 | . . . . . . . . 9
⊢ ((𝐺 Fn On ∧ 𝐶 ⊆ On) → (𝐺 ↾ 𝐶) Fn 𝐶) | 
| 11 | 7, 9, 10 | sylancr 587 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → (𝐺 ↾ 𝐶) Fn 𝐶) | 
| 12 | 11 | fndmd 6673 | . . . . . . 7
⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → dom (𝐺 ↾ 𝐶) = 𝐶) | 
| 13 | 6, 12 | eqtrd 2777 | . . . . . 6
⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → dom 𝑧 = 𝐶) | 
| 14 | 13 | unieqd 4920 | . . . . . 6
⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → ∪ dom
𝑧 = ∪ 𝐶) | 
| 15 | 13, 14 | eqeq12d 2753 | . . . . 5
⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → (dom 𝑧 = ∪ dom 𝑧 ↔ 𝐶 = ∪ 𝐶)) | 
| 16 | 13 | eqeq1d 2739 | . . . . . 6
⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → (dom 𝑧 = ∅ ↔ 𝐶 = ∅)) | 
| 17 | 5 | rneqd 5949 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → ran 𝑧 = ran (𝐺 ↾ 𝐶)) | 
| 18 |  | df-ima 5698 | . . . . . . . 8
⊢ (𝐺 “ 𝐶) = ran (𝐺 ↾ 𝐶) | 
| 19 | 17, 18 | eqtr4di 2795 | . . . . . . 7
⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → ran 𝑧 = (𝐺 “ 𝐶)) | 
| 20 | 19 | unieqd 4920 | . . . . . 6
⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → ∪ ran
𝑧 = ∪ (𝐺
“ 𝐶)) | 
| 21 | 16, 20 | ifbieq2d 4552 | . . . . 5
⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → if(dom 𝑧 = ∅, 𝐵, ∪ ran 𝑧) = if(𝐶 = ∅, 𝐵, ∪ (𝐺 “ 𝐶))) | 
| 22 | 5, 14 | fveq12d 6913 | . . . . . 6
⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → (𝑧‘∪ dom 𝑧) = ((𝐺 ↾ 𝐶)‘∪ 𝐶)) | 
| 23 | 14 | fveq2d 6910 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → (𝐹‘∪ dom
𝑧) = (𝐹‘∪ 𝐶)) | 
| 24 | 23 | sneqd 4638 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → {(𝐹‘∪ dom
𝑧)} = {(𝐹‘∪ 𝐶)}) | 
| 25 | 22, 24 | uneq12d 4169 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → ((𝑧‘∪ dom 𝑧) ∪ {(𝐹‘∪ dom
𝑧)}) = (((𝐺 ↾ 𝐶)‘∪ 𝐶) ∪ {(𝐹‘∪ 𝐶)})) | 
| 26 | 25 | eleq1d 2826 | . . . . . . 7
⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → (((𝑧‘∪ dom 𝑧) ∪ {(𝐹‘∪ dom
𝑧)}) ∈ 𝐴 ↔ (((𝐺 ↾ 𝐶)‘∪ 𝐶) ∪ {(𝐹‘∪ 𝐶)}) ∈ 𝐴)) | 
| 27 |  | eqidd 2738 | . . . . . . 7
⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → ∅ =
∅) | 
| 28 | 26, 24, 27 | ifbieq12d 4554 | . . . . . 6
⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → if(((𝑧‘∪ dom 𝑧) ∪ {(𝐹‘∪ dom
𝑧)}) ∈ 𝐴, {(𝐹‘∪ dom
𝑧)}, ∅) = if((((𝐺 ↾ 𝐶)‘∪ 𝐶) ∪ {(𝐹‘∪ 𝐶)}) ∈ 𝐴, {(𝐹‘∪ 𝐶)}, ∅)) | 
| 29 | 22, 28 | uneq12d 4169 | . . . . 5
⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → ((𝑧‘∪ dom 𝑧) ∪ if(((𝑧‘∪ dom 𝑧) ∪ {(𝐹‘∪ dom
𝑧)}) ∈ 𝐴, {(𝐹‘∪ dom
𝑧)}, ∅)) = (((𝐺 ↾ 𝐶)‘∪ 𝐶) ∪ if((((𝐺 ↾ 𝐶)‘∪ 𝐶) ∪ {(𝐹‘∪ 𝐶)}) ∈ 𝐴, {(𝐹‘∪ 𝐶)}, ∅))) | 
| 30 | 15, 21, 29 | ifbieq12d 4554 | . . . 4
⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → if(dom 𝑧 = ∪ dom 𝑧, if(dom 𝑧 = ∅, 𝐵, ∪ ran 𝑧), ((𝑧‘∪ dom 𝑧) ∪ if(((𝑧‘∪ dom 𝑧) ∪ {(𝐹‘∪ dom
𝑧)}) ∈ 𝐴, {(𝐹‘∪ dom
𝑧)}, ∅))) = if(𝐶 = ∪
𝐶, if(𝐶 = ∅, 𝐵, ∪ (𝐺 “ 𝐶)), (((𝐺 ↾ 𝐶)‘∪ 𝐶) ∪ if((((𝐺 ↾ 𝐶)‘∪ 𝐶) ∪ {(𝐹‘∪ 𝐶)}) ∈ 𝐴, {(𝐹‘∪ 𝐶)}, ∅)))) | 
| 31 |  | onuni 7808 | . . . . . . . . . 10
⊢ (𝐶 ∈ On → ∪ 𝐶
∈ On) | 
| 32 | 31 | ad3antlr 731 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → ∪ 𝐶
∈ On) | 
| 33 |  | sucidg 6465 | . . . . . . . . 9
⊢ (∪ 𝐶
∈ On → ∪ 𝐶 ∈ suc ∪
𝐶) | 
| 34 | 32, 33 | syl 17 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → ∪ 𝐶
∈ suc ∪ 𝐶) | 
| 35 |  | eloni 6394 | . . . . . . . . . . 11
⊢ (𝐶 ∈ On → Ord 𝐶) | 
| 36 | 35 | ad2antlr 727 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → Ord 𝐶) | 
| 37 |  | orduniorsuc 7850 | . . . . . . . . . 10
⊢ (Ord
𝐶 → (𝐶 = ∪ 𝐶 ∨ 𝐶 = suc ∪ 𝐶)) | 
| 38 | 36, 37 | syl 17 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → (𝐶 = ∪ 𝐶 ∨ 𝐶 = suc ∪ 𝐶)) | 
| 39 | 38 | orcanai 1005 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → 𝐶 = suc ∪ 𝐶) | 
| 40 | 34, 39 | eleqtrrd 2844 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → ∪ 𝐶
∈ 𝐶) | 
| 41 | 40 | fvresd 6926 | . . . . . 6
⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → ((𝐺 ↾ 𝐶)‘∪ 𝐶) = (𝐺‘∪ 𝐶)) | 
| 42 | 41 | uneq1d 4167 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → (((𝐺 ↾ 𝐶)‘∪ 𝐶) ∪ {(𝐹‘∪ 𝐶)}) = ((𝐺‘∪ 𝐶) ∪ {(𝐹‘∪ 𝐶)})) | 
| 43 | 42 | eleq1d 2826 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → ((((𝐺 ↾ 𝐶)‘∪ 𝐶) ∪ {(𝐹‘∪ 𝐶)}) ∈ 𝐴 ↔ ((𝐺‘∪ 𝐶) ∪ {(𝐹‘∪ 𝐶)}) ∈ 𝐴)) | 
| 44 | 43 | ifbid 4549 | . . . . . 6
⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → if((((𝐺 ↾ 𝐶)‘∪ 𝐶) ∪ {(𝐹‘∪ 𝐶)}) ∈ 𝐴, {(𝐹‘∪ 𝐶)}, ∅) = if(((𝐺‘∪ 𝐶)
∪ {(𝐹‘∪ 𝐶)})
∈ 𝐴, {(𝐹‘∪ 𝐶)},
∅)) | 
| 45 | 41, 44 | uneq12d 4169 | . . . . 5
⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) ∧ ¬ 𝐶 = ∪ 𝐶) → (((𝐺 ↾ 𝐶)‘∪ 𝐶) ∪ if((((𝐺 ↾ 𝐶)‘∪ 𝐶) ∪ {(𝐹‘∪ 𝐶)}) ∈ 𝐴, {(𝐹‘∪ 𝐶)}, ∅)) = ((𝐺‘∪ 𝐶)
∪ if(((𝐺‘∪ 𝐶)
∪ {(𝐹‘∪ 𝐶)})
∈ 𝐴, {(𝐹‘∪ 𝐶)},
∅))) | 
| 46 | 45 | ifeq2da 4558 | . . . 4
⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → if(𝐶 = ∪ 𝐶, if(𝐶 = ∅, 𝐵, ∪ (𝐺 “ 𝐶)), (((𝐺 ↾ 𝐶)‘∪ 𝐶) ∪ if((((𝐺 ↾ 𝐶)‘∪ 𝐶) ∪ {(𝐹‘∪ 𝐶)}) ∈ 𝐴, {(𝐹‘∪ 𝐶)}, ∅))) = if(𝐶 = ∪
𝐶, if(𝐶 = ∅, 𝐵, ∪ (𝐺 “ 𝐶)), ((𝐺‘∪ 𝐶) ∪ if(((𝐺‘∪ 𝐶) ∪ {(𝐹‘∪ 𝐶)}) ∈ 𝐴, {(𝐹‘∪ 𝐶)}, ∅)))) | 
| 47 | 30, 46 | eqtrd 2777 | . . 3
⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑧 = (𝐺 ↾ 𝐶)) → if(dom 𝑧 = ∪ dom 𝑧, if(dom 𝑧 = ∅, 𝐵, ∪ ran 𝑧), ((𝑧‘∪ dom 𝑧) ∪ if(((𝑧‘∪ dom 𝑧) ∪ {(𝐹‘∪ dom
𝑧)}) ∈ 𝐴, {(𝐹‘∪ dom
𝑧)}, ∅))) = if(𝐶 = ∪
𝐶, if(𝐶 = ∅, 𝐵, ∪ (𝐺 “ 𝐶)), ((𝐺‘∪ 𝐶) ∪ if(((𝐺‘∪ 𝐶) ∪ {(𝐹‘∪ 𝐶)}) ∈ 𝐴, {(𝐹‘∪ 𝐶)}, ∅)))) | 
| 48 |  | fnfun 6668 | . . . . 5
⊢ (𝐺 Fn On → Fun 𝐺) | 
| 49 | 7, 48 | ax-mp 5 | . . . 4
⊢ Fun 𝐺 | 
| 50 |  | simpr 484 | . . . 4
⊢ ((𝜑 ∧ 𝐶 ∈ On) → 𝐶 ∈ On) | 
| 51 |  | resfunexg 7235 | . . . 4
⊢ ((Fun
𝐺 ∧ 𝐶 ∈ On) → (𝐺 ↾ 𝐶) ∈ V) | 
| 52 | 49, 50, 51 | sylancr 587 | . . 3
⊢ ((𝜑 ∧ 𝐶 ∈ On) → (𝐺 ↾ 𝐶) ∈ V) | 
| 53 |  | ttukeylem.2 | . . . . . 6
⊢ (𝜑 → 𝐵 ∈ 𝐴) | 
| 54 | 53 | elexd 3504 | . . . . 5
⊢ (𝜑 → 𝐵 ∈ V) | 
| 55 |  | funimaexg 6653 | . . . . . . 7
⊢ ((Fun
𝐺 ∧ 𝐶 ∈ On) → (𝐺 “ 𝐶) ∈ V) | 
| 56 | 49, 55 | mpan 690 | . . . . . 6
⊢ (𝐶 ∈ On → (𝐺 “ 𝐶) ∈ V) | 
| 57 | 56 | uniexd 7762 | . . . . 5
⊢ (𝐶 ∈ On → ∪ (𝐺
“ 𝐶) ∈
V) | 
| 58 |  | ifcl 4571 | . . . . 5
⊢ ((𝐵 ∈ V ∧ ∪ (𝐺
“ 𝐶) ∈ V) →
if(𝐶 = ∅, 𝐵, ∪
(𝐺 “ 𝐶)) ∈ V) | 
| 59 | 54, 57, 58 | syl2an 596 | . . . 4
⊢ ((𝜑 ∧ 𝐶 ∈ On) → if(𝐶 = ∅, 𝐵, ∪ (𝐺 “ 𝐶)) ∈ V) | 
| 60 |  | fvex 6919 | . . . . 5
⊢ (𝐺‘∪ 𝐶)
∈ V | 
| 61 |  | snex 5436 | . . . . . 6
⊢ {(𝐹‘∪ 𝐶)}
∈ V | 
| 62 |  | 0ex 5307 | . . . . . 6
⊢ ∅
∈ V | 
| 63 | 61, 62 | ifex 4576 | . . . . 5
⊢
if(((𝐺‘∪ 𝐶)
∪ {(𝐹‘∪ 𝐶)})
∈ 𝐴, {(𝐹‘∪ 𝐶)},
∅) ∈ V | 
| 64 | 60, 63 | unex 7764 | . . . 4
⊢ ((𝐺‘∪ 𝐶)
∪ if(((𝐺‘∪ 𝐶)
∪ {(𝐹‘∪ 𝐶)})
∈ 𝐴, {(𝐹‘∪ 𝐶)},
∅)) ∈ V | 
| 65 |  | ifcl 4571 | . . . 4
⊢
((if(𝐶 = ∅,
𝐵, ∪ (𝐺
“ 𝐶)) ∈ V ∧
((𝐺‘∪ 𝐶)
∪ if(((𝐺‘∪ 𝐶)
∪ {(𝐹‘∪ 𝐶)})
∈ 𝐴, {(𝐹‘∪ 𝐶)},
∅)) ∈ V) → if(𝐶 = ∪ 𝐶, if(𝐶 = ∅, 𝐵, ∪ (𝐺 “ 𝐶)), ((𝐺‘∪ 𝐶) ∪ if(((𝐺‘∪ 𝐶) ∪ {(𝐹‘∪ 𝐶)}) ∈ 𝐴, {(𝐹‘∪ 𝐶)}, ∅))) ∈
V) | 
| 66 | 59, 64, 65 | sylancl 586 | . . 3
⊢ ((𝜑 ∧ 𝐶 ∈ On) → if(𝐶 = ∪ 𝐶, if(𝐶 = ∅, 𝐵, ∪ (𝐺 “ 𝐶)), ((𝐺‘∪ 𝐶) ∪ if(((𝐺‘∪ 𝐶) ∪ {(𝐹‘∪ 𝐶)}) ∈ 𝐴, {(𝐹‘∪ 𝐶)}, ∅))) ∈
V) | 
| 67 | 4, 47, 52, 66 | fvmptd 7023 | . 2
⊢ ((𝜑 ∧ 𝐶 ∈ On) → ((𝑧 ∈ V ↦ if(dom 𝑧 = ∪ dom 𝑧, if(dom 𝑧 = ∅, 𝐵, ∪ ran 𝑧), ((𝑧‘∪ dom 𝑧) ∪ if(((𝑧‘∪ dom 𝑧) ∪ {(𝐹‘∪ dom
𝑧)}) ∈ 𝐴, {(𝐹‘∪ dom
𝑧)},
∅))))‘(𝐺
↾ 𝐶)) = if(𝐶 = ∪
𝐶, if(𝐶 = ∅, 𝐵, ∪ (𝐺 “ 𝐶)), ((𝐺‘∪ 𝐶) ∪ if(((𝐺‘∪ 𝐶) ∪ {(𝐹‘∪ 𝐶)}) ∈ 𝐴, {(𝐹‘∪ 𝐶)}, ∅)))) | 
| 68 | 3, 67 | eqtrd 2777 | 1
⊢ ((𝜑 ∧ 𝐶 ∈ On) → (𝐺‘𝐶) = if(𝐶 = ∪ 𝐶, if(𝐶 = ∅, 𝐵, ∪ (𝐺 “ 𝐶)), ((𝐺‘∪ 𝐶) ∪ if(((𝐺‘∪ 𝐶) ∪ {(𝐹‘∪ 𝐶)}) ∈ 𝐴, {(𝐹‘∪ 𝐶)}, ∅)))) |