| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | sseq2 4009 | . . . . . 6
⊢ (𝑦 = 𝑎 → (𝐶 ⊆ 𝑦 ↔ 𝐶 ⊆ 𝑎)) | 
| 2 |  | fveq2 6905 | . . . . . . 7
⊢ (𝑦 = 𝑎 → (𝐺‘𝑦) = (𝐺‘𝑎)) | 
| 3 | 2 | sseq2d 4015 | . . . . . 6
⊢ (𝑦 = 𝑎 → ((𝐺‘𝐶) ⊆ (𝐺‘𝑦) ↔ (𝐺‘𝐶) ⊆ (𝐺‘𝑎))) | 
| 4 | 1, 3 | imbi12d 344 | . . . . 5
⊢ (𝑦 = 𝑎 → ((𝐶 ⊆ 𝑦 → (𝐺‘𝐶) ⊆ (𝐺‘𝑦)) ↔ (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)))) | 
| 5 | 4 | imbi2d 340 | . . . 4
⊢ (𝑦 = 𝑎 → (((𝜑 ∧ 𝐶 ∈ On) → (𝐶 ⊆ 𝑦 → (𝐺‘𝐶) ⊆ (𝐺‘𝑦))) ↔ ((𝜑 ∧ 𝐶 ∈ On) → (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎))))) | 
| 6 |  | sseq2 4009 | . . . . . 6
⊢ (𝑦 = 𝐷 → (𝐶 ⊆ 𝑦 ↔ 𝐶 ⊆ 𝐷)) | 
| 7 |  | fveq2 6905 | . . . . . . 7
⊢ (𝑦 = 𝐷 → (𝐺‘𝑦) = (𝐺‘𝐷)) | 
| 8 | 7 | sseq2d 4015 | . . . . . 6
⊢ (𝑦 = 𝐷 → ((𝐺‘𝐶) ⊆ (𝐺‘𝑦) ↔ (𝐺‘𝐶) ⊆ (𝐺‘𝐷))) | 
| 9 | 6, 8 | imbi12d 344 | . . . . 5
⊢ (𝑦 = 𝐷 → ((𝐶 ⊆ 𝑦 → (𝐺‘𝐶) ⊆ (𝐺‘𝑦)) ↔ (𝐶 ⊆ 𝐷 → (𝐺‘𝐶) ⊆ (𝐺‘𝐷)))) | 
| 10 | 9 | imbi2d 340 | . . . 4
⊢ (𝑦 = 𝐷 → (((𝜑 ∧ 𝐶 ∈ On) → (𝐶 ⊆ 𝑦 → (𝐺‘𝐶) ⊆ (𝐺‘𝑦))) ↔ ((𝜑 ∧ 𝐶 ∈ On) → (𝐶 ⊆ 𝐷 → (𝐺‘𝐶) ⊆ (𝐺‘𝐷))))) | 
| 11 |  | r19.21v 3179 | . . . . 5
⊢
(∀𝑎 ∈
𝑦 ((𝜑 ∧ 𝐶 ∈ On) → (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎))) ↔ ((𝜑 ∧ 𝐶 ∈ On) → ∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)))) | 
| 12 |  | onsseleq 6424 | . . . . . . . . . 10
⊢ ((𝐶 ∈ On ∧ 𝑦 ∈ On) → (𝐶 ⊆ 𝑦 ↔ (𝐶 ∈ 𝑦 ∨ 𝐶 = 𝑦))) | 
| 13 | 12 | ad4ant23 753 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ ∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎))) → (𝐶 ⊆ 𝑦 ↔ (𝐶 ∈ 𝑦 ∨ 𝐶 = 𝑦))) | 
| 14 |  | sseq2 4009 | . . . . . . . . . . . . 13
⊢ (if(𝑦 = ∅, 𝐵, ∪ (𝐺 “ 𝑦)) = if(𝑦 = ∪ 𝑦, if(𝑦 = ∅, 𝐵, ∪ (𝐺 “ 𝑦)), ((𝐺‘∪ 𝑦) ∪ if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅))) → ((𝐺‘𝐶) ⊆ if(𝑦 = ∅, 𝐵, ∪ (𝐺 “ 𝑦)) ↔ (𝐺‘𝐶) ⊆ if(𝑦 = ∪ 𝑦, if(𝑦 = ∅, 𝐵, ∪ (𝐺 “ 𝑦)), ((𝐺‘∪ 𝑦) ∪ if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)},
∅))))) | 
| 15 |  | sseq2 4009 | . . . . . . . . . . . . 13
⊢ (((𝐺‘∪ 𝑦)
∪ if(((𝐺‘∪ 𝑦)
∪ {(𝐹‘∪ 𝑦)})
∈ 𝐴, {(𝐹‘∪ 𝑦)},
∅)) = if(𝑦 = ∪ 𝑦,
if(𝑦 = ∅, 𝐵, ∪
(𝐺 “ 𝑦)), ((𝐺‘∪ 𝑦) ∪ if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅))) → ((𝐺‘𝐶) ⊆ ((𝐺‘∪ 𝑦) ∪ if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅)) ↔ (𝐺‘𝐶) ⊆ if(𝑦 = ∪ 𝑦, if(𝑦 = ∅, 𝐵, ∪ (𝐺 “ 𝑦)), ((𝐺‘∪ 𝑦) ∪ if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)},
∅))))) | 
| 16 |  | ttukeylem.4 | . . . . . . . . . . . . . . . . . 18
⊢ 𝐺 = recs((𝑧 ∈ V ↦ if(dom 𝑧 = ∪ dom 𝑧, if(dom 𝑧 = ∅, 𝐵, ∪ ran 𝑧), ((𝑧‘∪ dom 𝑧) ∪ if(((𝑧‘∪ dom 𝑧) ∪ {(𝐹‘∪ dom
𝑧)}) ∈ 𝐴, {(𝐹‘∪ dom
𝑧)},
∅))))) | 
| 17 | 16 | tfr1 8438 | . . . . . . . . . . . . . . . . 17
⊢ 𝐺 Fn On | 
| 18 |  | simplr 768 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ∧ 𝐶 ∈ 𝑦)) → 𝑦 ∈ On) | 
| 19 |  | onss 7806 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ On → 𝑦 ⊆ On) | 
| 20 | 18, 19 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ∧ 𝐶 ∈ 𝑦)) → 𝑦 ⊆ On) | 
| 21 |  | simprr 772 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ∧ 𝐶 ∈ 𝑦)) → 𝐶 ∈ 𝑦) | 
| 22 |  | fnfvima 7254 | . . . . . . . . . . . . . . . . 17
⊢ ((𝐺 Fn On ∧ 𝑦 ⊆ On ∧ 𝐶 ∈ 𝑦) → (𝐺‘𝐶) ∈ (𝐺 “ 𝑦)) | 
| 23 | 17, 20, 21, 22 | mp3an2i 1467 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ∧ 𝐶 ∈ 𝑦)) → (𝐺‘𝐶) ∈ (𝐺 “ 𝑦)) | 
| 24 |  | elssuni 4936 | . . . . . . . . . . . . . . . 16
⊢ ((𝐺‘𝐶) ∈ (𝐺 “ 𝑦) → (𝐺‘𝐶) ⊆ ∪
(𝐺 “ 𝑦)) | 
| 25 | 23, 24 | syl 17 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ∧ 𝐶 ∈ 𝑦)) → (𝐺‘𝐶) ⊆ ∪
(𝐺 “ 𝑦)) | 
| 26 |  | n0i 4339 | . . . . . . . . . . . . . . . 16
⊢ (𝐶 ∈ 𝑦 → ¬ 𝑦 = ∅) | 
| 27 |  | iffalse 4533 | . . . . . . . . . . . . . . . 16
⊢ (¬
𝑦 = ∅ → if(𝑦 = ∅, 𝐵, ∪ (𝐺 “ 𝑦)) = ∪ (𝐺 “ 𝑦)) | 
| 28 | 21, 26, 27 | 3syl 18 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ∧ 𝐶 ∈ 𝑦)) → if(𝑦 = ∅, 𝐵, ∪ (𝐺 “ 𝑦)) = ∪ (𝐺 “ 𝑦)) | 
| 29 | 25, 28 | sseqtrrd 4020 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ∧ 𝐶 ∈ 𝑦)) → (𝐺‘𝐶) ⊆ if(𝑦 = ∅, 𝐵, ∪ (𝐺 “ 𝑦))) | 
| 30 | 29 | adantr 480 | . . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ∧ 𝐶 ∈ 𝑦)) ∧ 𝑦 = ∪ 𝑦) → (𝐺‘𝐶) ⊆ if(𝑦 = ∅, 𝐵, ∪ (𝐺 “ 𝑦))) | 
| 31 | 21 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ∧ 𝐶 ∈ 𝑦)) ∧ ¬ 𝑦 = ∪ 𝑦) → 𝐶 ∈ 𝑦) | 
| 32 |  | elssuni 4936 | . . . . . . . . . . . . . . . 16
⊢ (𝐶 ∈ 𝑦 → 𝐶 ⊆ ∪ 𝑦) | 
| 33 | 31, 32 | syl 17 | . . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ∧ 𝐶 ∈ 𝑦)) ∧ ¬ 𝑦 = ∪ 𝑦) → 𝐶 ⊆ ∪ 𝑦) | 
| 34 |  | sseq2 4009 | . . . . . . . . . . . . . . . . 17
⊢ (𝑎 = ∪
𝑦 → (𝐶 ⊆ 𝑎 ↔ 𝐶 ⊆ ∪ 𝑦)) | 
| 35 |  | fveq2 6905 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑎 = ∪
𝑦 → (𝐺‘𝑎) = (𝐺‘∪ 𝑦)) | 
| 36 | 35 | sseq2d 4015 | . . . . . . . . . . . . . . . . 17
⊢ (𝑎 = ∪
𝑦 → ((𝐺‘𝐶) ⊆ (𝐺‘𝑎) ↔ (𝐺‘𝐶) ⊆ (𝐺‘∪ 𝑦))) | 
| 37 | 34, 36 | imbi12d 344 | . . . . . . . . . . . . . . . 16
⊢ (𝑎 = ∪
𝑦 → ((𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ↔ (𝐶 ⊆ ∪ 𝑦 → (𝐺‘𝐶) ⊆ (𝐺‘∪ 𝑦)))) | 
| 38 |  | simplrl 776 | . . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ∧ 𝐶 ∈ 𝑦)) ∧ ¬ 𝑦 = ∪ 𝑦) → ∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎))) | 
| 39 |  | vuniex 7760 | . . . . . . . . . . . . . . . . . 18
⊢ ∪ 𝑦
∈ V | 
| 40 | 39 | sucid 6465 | . . . . . . . . . . . . . . . . 17
⊢ ∪ 𝑦
∈ suc ∪ 𝑦 | 
| 41 |  | eloni 6393 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ On → Ord 𝑦) | 
| 42 |  | orduniorsuc 7851 | . . . . . . . . . . . . . . . . . . 19
⊢ (Ord
𝑦 → (𝑦 = ∪
𝑦 ∨ 𝑦 = suc ∪ 𝑦)) | 
| 43 | 18, 41, 42 | 3syl 18 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ∧ 𝐶 ∈ 𝑦)) → (𝑦 = ∪ 𝑦 ∨ 𝑦 = suc ∪ 𝑦)) | 
| 44 | 43 | orcanai 1004 | . . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ∧ 𝐶 ∈ 𝑦)) ∧ ¬ 𝑦 = ∪ 𝑦) → 𝑦 = suc ∪ 𝑦) | 
| 45 | 40, 44 | eleqtrrid 2847 | . . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ∧ 𝐶 ∈ 𝑦)) ∧ ¬ 𝑦 = ∪ 𝑦) → ∪ 𝑦
∈ 𝑦) | 
| 46 | 37, 38, 45 | rspcdva 3622 | . . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ∧ 𝐶 ∈ 𝑦)) ∧ ¬ 𝑦 = ∪ 𝑦) → (𝐶 ⊆ ∪ 𝑦 → (𝐺‘𝐶) ⊆ (𝐺‘∪ 𝑦))) | 
| 47 | 33, 46 | mpd 15 | . . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ∧ 𝐶 ∈ 𝑦)) ∧ ¬ 𝑦 = ∪ 𝑦) → (𝐺‘𝐶) ⊆ (𝐺‘∪ 𝑦)) | 
| 48 |  | ssun1 4177 | . . . . . . . . . . . . . 14
⊢ (𝐺‘∪ 𝑦)
⊆ ((𝐺‘∪ 𝑦)
∪ if(((𝐺‘∪ 𝑦)
∪ {(𝐹‘∪ 𝑦)})
∈ 𝐴, {(𝐹‘∪ 𝑦)},
∅)) | 
| 49 | 47, 48 | sstrdi 3995 | . . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ∧ 𝐶 ∈ 𝑦)) ∧ ¬ 𝑦 = ∪ 𝑦) → (𝐺‘𝐶) ⊆ ((𝐺‘∪ 𝑦) ∪ if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅))) | 
| 50 | 14, 15, 30, 49 | ifbothda 4563 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ∧ 𝐶 ∈ 𝑦)) → (𝐺‘𝐶) ⊆ if(𝑦 = ∪ 𝑦, if(𝑦 = ∅, 𝐵, ∪ (𝐺 “ 𝑦)), ((𝐺‘∪ 𝑦) ∪ if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅)))) | 
| 51 |  | ttukeylem.1 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐹:(card‘(∪
𝐴 ∖ 𝐵))–1-1-onto→(∪ 𝐴 ∖ 𝐵)) | 
| 52 |  | ttukeylem.2 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐵 ∈ 𝐴) | 
| 53 |  | ttukeylem.3 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 ↔ (𝒫 𝑥 ∩ Fin) ⊆ 𝐴)) | 
| 54 | 51, 52, 53, 16 | ttukeylem3 10552 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ On) → (𝐺‘𝑦) = if(𝑦 = ∪ 𝑦, if(𝑦 = ∅, 𝐵, ∪ (𝐺 “ 𝑦)), ((𝐺‘∪ 𝑦) ∪ if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅)))) | 
| 55 | 54 | ad4ant13 751 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ∧ 𝐶 ∈ 𝑦)) → (𝐺‘𝑦) = if(𝑦 = ∪ 𝑦, if(𝑦 = ∅, 𝐵, ∪ (𝐺 “ 𝑦)), ((𝐺‘∪ 𝑦) ∪ if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅)))) | 
| 56 | 50, 55 | sseqtrrd 4020 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ∧ 𝐶 ∈ 𝑦)) → (𝐺‘𝐶) ⊆ (𝐺‘𝑦)) | 
| 57 | 56 | expr 456 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ ∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎))) → (𝐶 ∈ 𝑦 → (𝐺‘𝐶) ⊆ (𝐺‘𝑦))) | 
| 58 |  | fveq2 6905 | . . . . . . . . . . . 12
⊢ (𝐶 = 𝑦 → (𝐺‘𝐶) = (𝐺‘𝑦)) | 
| 59 |  | eqimss 4041 | . . . . . . . . . . . 12
⊢ ((𝐺‘𝐶) = (𝐺‘𝑦) → (𝐺‘𝐶) ⊆ (𝐺‘𝑦)) | 
| 60 | 58, 59 | syl 17 | . . . . . . . . . . 11
⊢ (𝐶 = 𝑦 → (𝐺‘𝐶) ⊆ (𝐺‘𝑦)) | 
| 61 | 60 | a1i 11 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ ∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎))) → (𝐶 = 𝑦 → (𝐺‘𝐶) ⊆ (𝐺‘𝑦))) | 
| 62 | 57, 61 | jaod 859 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ ∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎))) → ((𝐶 ∈ 𝑦 ∨ 𝐶 = 𝑦) → (𝐺‘𝐶) ⊆ (𝐺‘𝑦))) | 
| 63 | 13, 62 | sylbid 240 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ ∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎))) → (𝐶 ⊆ 𝑦 → (𝐺‘𝐶) ⊆ (𝐺‘𝑦))) | 
| 64 | 63 | ex 412 | . . . . . . 7
⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) → (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) → (𝐶 ⊆ 𝑦 → (𝐺‘𝐶) ⊆ (𝐺‘𝑦)))) | 
| 65 | 64 | expcom 413 | . . . . . 6
⊢ (𝑦 ∈ On → ((𝜑 ∧ 𝐶 ∈ On) → (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) → (𝐶 ⊆ 𝑦 → (𝐺‘𝐶) ⊆ (𝐺‘𝑦))))) | 
| 66 | 65 | a2d 29 | . . . . 5
⊢ (𝑦 ∈ On → (((𝜑 ∧ 𝐶 ∈ On) → ∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎))) → ((𝜑 ∧ 𝐶 ∈ On) → (𝐶 ⊆ 𝑦 → (𝐺‘𝐶) ⊆ (𝐺‘𝑦))))) | 
| 67 | 11, 66 | biimtrid 242 | . . . 4
⊢ (𝑦 ∈ On → (∀𝑎 ∈ 𝑦 ((𝜑 ∧ 𝐶 ∈ On) → (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎))) → ((𝜑 ∧ 𝐶 ∈ On) → (𝐶 ⊆ 𝑦 → (𝐺‘𝐶) ⊆ (𝐺‘𝑦))))) | 
| 68 | 5, 10, 67 | tfis3 7880 | . . 3
⊢ (𝐷 ∈ On → ((𝜑 ∧ 𝐶 ∈ On) → (𝐶 ⊆ 𝐷 → (𝐺‘𝐶) ⊆ (𝐺‘𝐷)))) | 
| 69 | 68 | expdcom 414 | . 2
⊢ (𝜑 → (𝐶 ∈ On → (𝐷 ∈ On → (𝐶 ⊆ 𝐷 → (𝐺‘𝐶) ⊆ (𝐺‘𝐷))))) | 
| 70 | 69 | 3imp2 1349 | 1
⊢ ((𝜑 ∧ (𝐶 ∈ On ∧ 𝐷 ∈ On ∧ 𝐶 ⊆ 𝐷)) → (𝐺‘𝐶) ⊆ (𝐺‘𝐷)) |