Theorem ttukeylem5 10582

Description: Lemma for ttukey 10587. The 𝐺 function forms a (transfinitely long) chain of inclusions. (Contributed by Mario Carneiro, 15-May-2015.)

Hypotheses

Ref	Expression
ttukeylem.1	⊢ (𝜑 → 𝐹:(card‘(∪ 𝐴 ∖ 𝐵))–1-1-onto→(∪ 𝐴 ∖ 𝐵))
ttukeylem.2	⊢ (𝜑 → 𝐵 ∈ 𝐴)
ttukeylem.3	⊢ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 ↔ (𝒫 𝑥 ∩ Fin) ⊆ 𝐴))
ttukeylem.4	⊢ 𝐺 = recs((𝑧 ∈ V ↦ if(dom 𝑧 = ∪ dom 𝑧, if(dom 𝑧 = ∅, 𝐵, ∪ ran 𝑧), ((𝑧‘∪ dom 𝑧) ∪ if(((𝑧‘∪ dom 𝑧) ∪ {(𝐹‘∪ dom 𝑧)}) ∈ 𝐴, {(𝐹‘∪ dom 𝑧)}, ∅)))))

Assertion

Ref	Expression
ttukeylem5	⊢ ((𝜑 ∧ (𝐶 ∈ On ∧ 𝐷 ∈ On ∧ 𝐶 ⊆ 𝐷)) → (𝐺‘𝐶) ⊆ (𝐺‘𝐷))

Distinct variable groups:   𝑥,𝑧,𝐶   𝑥,𝐷   𝑥,𝐺,𝑧   𝜑,𝑧   𝑥,𝐴,𝑧   𝑥,𝐵,𝑧   𝑥,𝐹,𝑧

Allowed substitution hints:   𝜑(𝑥)   𝐷(𝑧)

Proof of Theorem ttukeylem5

Dummy variables 𝑎 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		sseq2 4035	. . . . . 6 ⊢ (𝑦 = 𝑎 → (𝐶 ⊆ 𝑦 ↔ 𝐶 ⊆ 𝑎))
2		fveq2 6920	. . . . . . 7 ⊢ (𝑦 = 𝑎 → (𝐺‘𝑦) = (𝐺‘𝑎))
3	2	sseq2d 4041	. . . . . 6 ⊢ (𝑦 = 𝑎 → ((𝐺‘𝐶) ⊆ (𝐺‘𝑦) ↔ (𝐺‘𝐶) ⊆ (𝐺‘𝑎)))
4	1, 3	imbi12d 344	. . . . 5 ⊢ (𝑦 = 𝑎 → ((𝐶 ⊆ 𝑦 → (𝐺‘𝐶) ⊆ (𝐺‘𝑦)) ↔ (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎))))
5	4	imbi2d 340	. . . 4 ⊢ (𝑦 = 𝑎 → (((𝜑 ∧ 𝐶 ∈ On) → (𝐶 ⊆ 𝑦 → (𝐺‘𝐶) ⊆ (𝐺‘𝑦))) ↔ ((𝜑 ∧ 𝐶 ∈ On) → (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)))))
6		sseq2 4035	. . . . . 6 ⊢ (𝑦 = 𝐷 → (𝐶 ⊆ 𝑦 ↔ 𝐶 ⊆ 𝐷))
7		fveq2 6920	. . . . . . 7 ⊢ (𝑦 = 𝐷 → (𝐺‘𝑦) = (𝐺‘𝐷))
8	7	sseq2d 4041	. . . . . 6 ⊢ (𝑦 = 𝐷 → ((𝐺‘𝐶) ⊆ (𝐺‘𝑦) ↔ (𝐺‘𝐶) ⊆ (𝐺‘𝐷)))
9	6, 8	imbi12d 344	. . . . 5 ⊢ (𝑦 = 𝐷 → ((𝐶 ⊆ 𝑦 → (𝐺‘𝐶) ⊆ (𝐺‘𝑦)) ↔ (𝐶 ⊆ 𝐷 → (𝐺‘𝐶) ⊆ (𝐺‘𝐷))))
10	9	imbi2d 340	. . . 4 ⊢ (𝑦 = 𝐷 → (((𝜑 ∧ 𝐶 ∈ On) → (𝐶 ⊆ 𝑦 → (𝐺‘𝐶) ⊆ (𝐺‘𝑦))) ↔ ((𝜑 ∧ 𝐶 ∈ On) → (𝐶 ⊆ 𝐷 → (𝐺‘𝐶) ⊆ (𝐺‘𝐷)))))
11		r19.21v 3186	. . . . 5 ⊢ (∀𝑎 ∈ 𝑦 ((𝜑 ∧ 𝐶 ∈ On) → (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎))) ↔ ((𝜑 ∧ 𝐶 ∈ On) → ∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎))))
12		onsseleq 6436	. . . . . . . . . 10 ⊢ ((𝐶 ∈ On ∧ 𝑦 ∈ On) → (𝐶 ⊆ 𝑦 ↔ (𝐶 ∈ 𝑦 ∨ 𝐶 = 𝑦)))
13	12	ad4ant23 752	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ ∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎))) → (𝐶 ⊆ 𝑦 ↔ (𝐶 ∈ 𝑦 ∨ 𝐶 = 𝑦)))
14		sseq2 4035	. . . . . . . . . . . . 13 ⊢ (if(𝑦 = ∅, 𝐵, ∪ (𝐺 “ 𝑦)) = if(𝑦 = ∪ 𝑦, if(𝑦 = ∅, 𝐵, ∪ (𝐺 “ 𝑦)), ((𝐺‘∪ 𝑦) ∪ if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅))) → ((𝐺‘𝐶) ⊆ if(𝑦 = ∅, 𝐵, ∪ (𝐺 “ 𝑦)) ↔ (𝐺‘𝐶) ⊆ if(𝑦 = ∪ 𝑦, if(𝑦 = ∅, 𝐵, ∪ (𝐺 “ 𝑦)), ((𝐺‘∪ 𝑦) ∪ if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅)))))
15		sseq2 4035	. . . . . . . . . . . . 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 8453	. . . . . . . . . . . . . . . . 17 ⊢ 𝐺 Fn On
18		simplr 768	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ∧ 𝐶 ∈ 𝑦)) → 𝑦 ∈ On)
19		onss 7820	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ On → 𝑦 ⊆ On)
20	18, 19	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ∧ 𝐶 ∈ 𝑦)) → 𝑦 ⊆ On)
21		simprr 772	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ∧ 𝐶 ∈ 𝑦)) → 𝐶 ∈ 𝑦)
22		fnfvima 7270	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐺 Fn On ∧ 𝑦 ⊆ On ∧ 𝐶 ∈ 𝑦) → (𝐺‘𝐶) ∈ (𝐺 “ 𝑦))
23	17, 20, 21, 22	mp3an2i 1466	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ∧ 𝐶 ∈ 𝑦)) → (𝐺‘𝐶) ∈ (𝐺 “ 𝑦))
24		elssuni 4961	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺‘𝐶) ∈ (𝐺 “ 𝑦) → (𝐺‘𝐶) ⊆ ∪ (𝐺 “ 𝑦))
25	23, 24	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ∧ 𝐶 ∈ 𝑦)) → (𝐺‘𝐶) ⊆ ∪ (𝐺 “ 𝑦))
26		n0i 4363	. . . . . . . . . . . . . . . 16 ⊢ (𝐶 ∈ 𝑦 → ¬ 𝑦 = ∅)
27		iffalse 4557	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝑦 = ∅ → if(𝑦 = ∅, 𝐵, ∪ (𝐺 “ 𝑦)) = ∪ (𝐺 “ 𝑦))
28	21, 26, 27	3syl 18	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ∧ 𝐶 ∈ 𝑦)) → if(𝑦 = ∅, 𝐵, ∪ (𝐺 “ 𝑦)) = ∪ (𝐺 “ 𝑦))
29	25, 28	sseqtrrd 4050	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ∧ 𝐶 ∈ 𝑦)) → (𝐺‘𝐶) ⊆ if(𝑦 = ∅, 𝐵, ∪ (𝐺 “ 𝑦)))
30	29	adantr 480	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ∧ 𝐶 ∈ 𝑦)) ∧ 𝑦 = ∪ 𝑦) → (𝐺‘𝐶) ⊆ if(𝑦 = ∅, 𝐵, ∪ (𝐺 “ 𝑦)))
31	21	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ∧ 𝐶 ∈ 𝑦)) ∧ ¬ 𝑦 = ∪ 𝑦) → 𝐶 ∈ 𝑦)
32		elssuni 4961	. . . . . . . . . . . . . . . 16 ⊢ (𝐶 ∈ 𝑦 → 𝐶 ⊆ ∪ 𝑦)
33	31, 32	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ∧ 𝐶 ∈ 𝑦)) ∧ ¬ 𝑦 = ∪ 𝑦) → 𝐶 ⊆ ∪ 𝑦)
34		sseq2 4035	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = ∪ 𝑦 → (𝐶 ⊆ 𝑎 ↔ 𝐶 ⊆ ∪ 𝑦))
35		fveq2 6920	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = ∪ 𝑦 → (𝐺‘𝑎) = (𝐺‘∪ 𝑦))
36	35	sseq2d 4041	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = ∪ 𝑦 → ((𝐺‘𝐶) ⊆ (𝐺‘𝑎) ↔ (𝐺‘𝐶) ⊆ (𝐺‘∪ 𝑦)))
37	34, 36	imbi12d 344	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = ∪ 𝑦 → ((𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ↔ (𝐶 ⊆ ∪ 𝑦 → (𝐺‘𝐶) ⊆ (𝐺‘∪ 𝑦))))
38		simplrl 776	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ∧ 𝐶 ∈ 𝑦)) ∧ ¬ 𝑦 = ∪ 𝑦) → ∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)))
39		vuniex 7774	. . . . . . . . . . . . . . . . . 18 ⊢ ∪ 𝑦 ∈ V
40	39	sucid 6477	. . . . . . . . . . . . . . . . 17 ⊢ ∪ 𝑦 ∈ suc ∪ 𝑦
41		eloni 6405	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ On → Ord 𝑦)
42		orduniorsuc 7866	. . . . . . . . . . . . . . . . . . 19 ⊢ (Ord 𝑦 → (𝑦 = ∪ 𝑦 ∨ 𝑦 = suc ∪ 𝑦))
43	18, 41, 42	3syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ∧ 𝐶 ∈ 𝑦)) → (𝑦 = ∪ 𝑦 ∨ 𝑦 = suc ∪ 𝑦))
44	43	orcanai 1003	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ∧ 𝐶 ∈ 𝑦)) ∧ ¬ 𝑦 = ∪ 𝑦) → 𝑦 = suc ∪ 𝑦)
45	40, 44	eleqtrrid 2851	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ∧ 𝐶 ∈ 𝑦)) ∧ ¬ 𝑦 = ∪ 𝑦) → ∪ 𝑦 ∈ 𝑦)
46	37, 38, 45	rspcdva 3636	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ∧ 𝐶 ∈ 𝑦)) ∧ ¬ 𝑦 = ∪ 𝑦) → (𝐶 ⊆ ∪ 𝑦 → (𝐺‘𝐶) ⊆ (𝐺‘∪ 𝑦)))
47	33, 46	mpd 15	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ∧ 𝐶 ∈ 𝑦)) ∧ ¬ 𝑦 = ∪ 𝑦) → (𝐺‘𝐶) ⊆ (𝐺‘∪ 𝑦))
48		ssun1 4201	. . . . . . . . . . . . . 14 ⊢ (𝐺‘∪ 𝑦) ⊆ ((𝐺‘∪ 𝑦) ∪ if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅))
49	47, 48	sstrdi 4021	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ∧ 𝐶 ∈ 𝑦)) ∧ ¬ 𝑦 = ∪ 𝑦) → (𝐺‘𝐶) ⊆ ((𝐺‘∪ 𝑦) ∪ if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅)))
50	14, 15, 30, 49	ifbothda 4586	. . . . . . . . . . . 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 10580	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ On) → (𝐺‘𝑦) = if(𝑦 = ∪ 𝑦, if(𝑦 = ∅, 𝐵, ∪ (𝐺 “ 𝑦)), ((𝐺‘∪ 𝑦) ∪ if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅))))
55	54	ad4ant13 750	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ∧ 𝐶 ∈ 𝑦)) → (𝐺‘𝑦) = if(𝑦 = ∪ 𝑦, if(𝑦 = ∅, 𝐵, ∪ (𝐺 “ 𝑦)), ((𝐺‘∪ 𝑦) ∪ if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅))))
56	50, 55	sseqtrrd 4050	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ∧ 𝐶 ∈ 𝑦)) → (𝐺‘𝐶) ⊆ (𝐺‘𝑦))
57	56	expr 456	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ ∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎))) → (𝐶 ∈ 𝑦 → (𝐺‘𝐶) ⊆ (𝐺‘𝑦)))
58		fveq2 6920	. . . . . . . . . . . 12 ⊢ (𝐶 = 𝑦 → (𝐺‘𝐶) = (𝐺‘𝑦))
59		eqimss 4067	. . . . . . . . . . . 12 ⊢ ((𝐺‘𝐶) = (𝐺‘𝑦) → (𝐺‘𝐶) ⊆ (𝐺‘𝑦))
60	58, 59	syl 17	. . . . . . . . . . 11 ⊢ (𝐶 = 𝑦 → (𝐺‘𝐶) ⊆ (𝐺‘𝑦))
61	60	a1i 11	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ ∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎))) → (𝐶 = 𝑦 → (𝐺‘𝐶) ⊆ (𝐺‘𝑦)))
62	57, 61	jaod 858	. . . . . . . . 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 7895	. . 3 ⊢ (𝐷 ∈ On → ((𝜑 ∧ 𝐶 ∈ On) → (𝐶 ⊆ 𝐷 → (𝐺‘𝐶) ⊆ (𝐺‘𝐷))))
69	68	expdcom 414	. 2 ⊢ (𝜑 → (𝐶 ∈ On → (𝐷 ∈ On → (𝐶 ⊆ 𝐷 → (𝐺‘𝐶) ⊆ (𝐺‘𝐷)))))
70	69	3imp2 1349	1 ⊢ ((𝜑 ∧ (𝐶 ∈ On ∧ 𝐷 ∈ On ∧ 𝐶 ⊆ 𝐷)) → (𝐺‘𝐶) ⊆ (𝐺‘𝐷))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 846   ∧ w3a 1087  ∀wal 1535   = wceq 1537   ∈ wcel 2108  ∀wral 3067  Vcvv 3488   ∖ cdif 3973   ∪ cun 3974   ∩ cin 3975   ⊆ wss 3976  ∅c0 4352  ifcif 4548  𝒫 cpw 4622  {csn 4648  ∪ cuni 4931   ↦ cmpt 5249  dom cdm 5700  ran crn 5701   “ cima 5703  Ord word 6394  Oncon0 6395  suc csuc 6397   Fn wfn 6568  –1-1-onto→wf1o 6572  ‘cfv 6573  recscrecs 8426  Fincfn 9003  cardccrd 10004

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-rep 5303  ax-sep 5317  ax-nul 5324  ax-pr 5447  ax-un 7770

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-ral 3068  df-rex 3077  df-reu 3389  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-pss 3996  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-iun 5017  df-br 5167  df-opab 5229  df-mpt 5250  df-tr 5284  df-id 5593  df-eprel 5599  df-po 5607  df-so 5608  df-fr 5652  df-we 5654  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-pred 6332  df-ord 6398  df-on 6399  df-suc 6401  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-ov 7451  df-2nd 8031  df-frecs 8322  df-wrecs 8353  df-recs 8427

This theorem is referenced by:  ttukeylem6  10583  ttukeylem7  10584