Theorem ttukeylem5 10485

Description: Lemma for ttukey 10490. 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 3965	. . . . . 6 ⊢ (𝑦 = 𝑎 → (𝐶 ⊆ 𝑦 ↔ 𝐶 ⊆ 𝑎))
2		fveq2 6871	. . . . . . 7 ⊢ (𝑦 = 𝑎 → (𝐺‘𝑦) = (𝐺‘𝑎))
3	2	sseq2d 3971	. . . . . 6 ⊢ (𝑦 = 𝑎 → ((𝐺‘𝐶) ⊆ (𝐺‘𝑦) ↔ (𝐺‘𝐶) ⊆ (𝐺‘𝑎)))
4	1, 3	imbi12d 347	. . . . 5 ⊢ (𝑦 = 𝑎 → ((𝐶 ⊆ 𝑦 → (𝐺‘𝐶) ⊆ (𝐺‘𝑦)) ↔ (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎))))
5	4	imbi2d 343	. . . 4 ⊢ (𝑦 = 𝑎 → (((𝜑 ∧ 𝐶 ∈ On) → (𝐶 ⊆ 𝑦 → (𝐺‘𝐶) ⊆ (𝐺‘𝑦))) ↔ ((𝜑 ∧ 𝐶 ∈ On) → (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)))))
6		sseq2 3965	. . . . . 6 ⊢ (𝑦 = 𝐷 → (𝐶 ⊆ 𝑦 ↔ 𝐶 ⊆ 𝐷))
7		fveq2 6871	. . . . . . 7 ⊢ (𝑦 = 𝐷 → (𝐺‘𝑦) = (𝐺‘𝐷))
8	7	sseq2d 3971	. . . . . 6 ⊢ (𝑦 = 𝐷 → ((𝐺‘𝐶) ⊆ (𝐺‘𝑦) ↔ (𝐺‘𝐶) ⊆ (𝐺‘𝐷)))
9	6, 8	imbi12d 347	. . . . 5 ⊢ (𝑦 = 𝐷 → ((𝐶 ⊆ 𝑦 → (𝐺‘𝐶) ⊆ (𝐺‘𝑦)) ↔ (𝐶 ⊆ 𝐷 → (𝐺‘𝐶) ⊆ (𝐺‘𝐷))))
10	9	imbi2d 343	. . . 4 ⊢ (𝑦 = 𝐷 → (((𝜑 ∧ 𝐶 ∈ On) → (𝐶 ⊆ 𝑦 → (𝐺‘𝐶) ⊆ (𝐺‘𝑦))) ↔ ((𝜑 ∧ 𝐶 ∈ On) → (𝐶 ⊆ 𝐷 → (𝐺‘𝐶) ⊆ (𝐺‘𝐷)))))
11		r19.21v 3190	. . . . 5 ⊢ (∀𝑎 ∈ 𝑦 ((𝜑 ∧ 𝐶 ∈ On) → (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎))) ↔ ((𝜑 ∧ 𝐶 ∈ On) → ∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎))))
12		onsseleq 6391	. . . . . . . . . 10 ⊢ ((𝐶 ∈ On ∧ 𝑦 ∈ On) → (𝐶 ⊆ 𝑦 ↔ (𝐶 ∈ 𝑦 ∨ 𝐶 = 𝑦)))
13	12	ad4ant23 765	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ ∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎))) → (𝐶 ⊆ 𝑦 ↔ (𝐶 ∈ 𝑦 ∨ 𝐶 = 𝑦)))
14		sseq2 3965	. . . . . . . . . . . . 13 ⊢ (if(𝑦 = ∅, 𝐵, ∪ (𝐺 “ 𝑦)) = if(𝑦 = ∪ 𝑦, if(𝑦 = ∅, 𝐵, ∪ (𝐺 “ 𝑦)), ((𝐺‘∪ 𝑦) ∪ if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅))) → ((𝐺‘𝐶) ⊆ if(𝑦 = ∅, 𝐵, ∪ (𝐺 “ 𝑦)) ↔ (𝐺‘𝐶) ⊆ if(𝑦 = ∪ 𝑦, if(𝑦 = ∅, 𝐵, ∪ (𝐺 “ 𝑦)), ((𝐺‘∪ 𝑦) ∪ if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅)))))
15		sseq2 3965	. . . . . . . . . . . . 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 8372	. . . . . . . . . . . . . . . . 17 ⊢ 𝐺 Fn On
18		simplr 780	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ∧ 𝐶 ∈ 𝑦)) → 𝑦 ∈ On)
19		onss 7772	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ On → 𝑦 ⊆ On)
20	18, 19	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ∧ 𝐶 ∈ 𝑦)) → 𝑦 ⊆ On)
21		simprr 784	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ∧ 𝐶 ∈ 𝑦)) → 𝐶 ∈ 𝑦)
22		fnfvima 7221	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐺 Fn On ∧ 𝑦 ⊆ On ∧ 𝐶 ∈ 𝑦) → (𝐺‘𝐶) ∈ (𝐺 “ 𝑦))
23	17, 20, 21, 22	mp3an2i 1490	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ∧ 𝐶 ∈ 𝑦)) → (𝐺‘𝐶) ∈ (𝐺 “ 𝑦))
24		elssuni 4900	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺‘𝐶) ∈ (𝐺 “ 𝑦) → (𝐺‘𝐶) ⊆ ∪ (𝐺 “ 𝑦))
25	23, 24	syl 18	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ∧ 𝐶 ∈ 𝑦)) → (𝐺‘𝐶) ⊆ ∪ (𝐺 “ 𝑦))
26		n0i 4295	. . . . . . . . . . . . . . . 16 ⊢ (𝐶 ∈ 𝑦 → ¬ 𝑦 = ∅)
27		iffalse 4492	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝑦 = ∅ → if(𝑦 = ∅, 𝐵, ∪ (𝐺 “ 𝑦)) = ∪ (𝐺 “ 𝑦))
28	21, 26, 27	3syl 19	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ∧ 𝐶 ∈ 𝑦)) → if(𝑦 = ∅, 𝐵, ∪ (𝐺 “ 𝑦)) = ∪ (𝐺 “ 𝑦))
29	25, 28	sseqtrrd 3976	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ∧ 𝐶 ∈ 𝑦)) → (𝐺‘𝐶) ⊆ if(𝑦 = ∅, 𝐵, ∪ (𝐺 “ 𝑦)))
30	29	adantr 485	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ∧ 𝐶 ∈ 𝑦)) ∧ 𝑦 = ∪ 𝑦) → (𝐺‘𝐶) ⊆ if(𝑦 = ∅, 𝐵, ∪ (𝐺 “ 𝑦)))
31	21	adantr 485	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ∧ 𝐶 ∈ 𝑦)) ∧ ¬ 𝑦 = ∪ 𝑦) → 𝐶 ∈ 𝑦)
32		elssuni 4900	. . . . . . . . . . . . . . . 16 ⊢ (𝐶 ∈ 𝑦 → 𝐶 ⊆ ∪ 𝑦)
33	31, 32	syl 18	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ∧ 𝐶 ∈ 𝑦)) ∧ ¬ 𝑦 = ∪ 𝑦) → 𝐶 ⊆ ∪ 𝑦)
34		sseq2 3965	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = ∪ 𝑦 → (𝐶 ⊆ 𝑎 ↔ 𝐶 ⊆ ∪ 𝑦))
35		fveq2 6871	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = ∪ 𝑦 → (𝐺‘𝑎) = (𝐺‘∪ 𝑦))
36	35	sseq2d 3971	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = ∪ 𝑦 → ((𝐺‘𝐶) ⊆ (𝐺‘𝑎) ↔ (𝐺‘𝐶) ⊆ (𝐺‘∪ 𝑦)))
37	34, 36	imbi12d 347	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = ∪ 𝑦 → ((𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ↔ (𝐶 ⊆ ∪ 𝑦 → (𝐺‘𝐶) ⊆ (𝐺‘∪ 𝑦))))
38		simplrl 788	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ∧ 𝐶 ∈ 𝑦)) ∧ ¬ 𝑦 = ∪ 𝑦) → ∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)))
39		vuniex 7726	. . . . . . . . . . . . . . . . . 18 ⊢ ∪ 𝑦 ∈ V
40	39	sucid 6434	. . . . . . . . . . . . . . . . 17 ⊢ ∪ 𝑦 ∈ suc ∪ 𝑦
41		eloni 6360	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ On → Ord 𝑦)
42		orduniorsuc 7814	. . . . . . . . . . . . . . . . . . 19 ⊢ (Ord 𝑦 → (𝑦 = ∪ 𝑦 ∨ 𝑦 = suc ∪ 𝑦))
43	18, 41, 42	3syl 19	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ∧ 𝐶 ∈ 𝑦)) → (𝑦 = ∪ 𝑦 ∨ 𝑦 = suc ∪ 𝑦))
44	43	orcanai 1018	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ∧ 𝐶 ∈ 𝑦)) ∧ ¬ 𝑦 = ∪ 𝑦) → 𝑦 = suc ∪ 𝑦)
45	40, 44	eleqtrrid 2872	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ∧ 𝐶 ∈ 𝑦)) ∧ ¬ 𝑦 = ∪ 𝑦) → ∪ 𝑦 ∈ 𝑦)
46	37, 38, 45	rspcdva 3585	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ∧ 𝐶 ∈ 𝑦)) ∧ ¬ 𝑦 = ∪ 𝑦) → (𝐶 ⊆ ∪ 𝑦 → (𝐺‘𝐶) ⊆ (𝐺‘∪ 𝑦)))
47	33, 46	mpd 16	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ∧ 𝐶 ∈ 𝑦)) ∧ ¬ 𝑦 = ∪ 𝑦) → (𝐺‘𝐶) ⊆ (𝐺‘∪ 𝑦))
48		ssun1 4133	. . . . . . . . . . . . . 14 ⊢ (𝐺‘∪ 𝑦) ⊆ ((𝐺‘∪ 𝑦) ∪ if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅))
49	47, 48	sstrdi 3951	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ∧ 𝐶 ∈ 𝑦)) ∧ ¬ 𝑦 = ∪ 𝑦) → (𝐺‘𝐶) ⊆ ((𝐺‘∪ 𝑦) ∪ if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅)))
50	14, 15, 30, 49	ifbothda 4522	. . . . . . . . . . . 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 10483	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ On) → (𝐺‘𝑦) = if(𝑦 = ∪ 𝑦, if(𝑦 = ∅, 𝐵, ∪ (𝐺 “ 𝑦)), ((𝐺‘∪ 𝑦) ∪ if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅))))
55	54	ad4ant13 763	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ∧ 𝐶 ∈ 𝑦)) → (𝐺‘𝑦) = if(𝑦 = ∪ 𝑦, if(𝑦 = ∅, 𝐵, ∪ (𝐺 “ 𝑦)), ((𝐺‘∪ 𝑦) ∪ if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅))))
56	50, 55	sseqtrrd 3976	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ∧ 𝐶 ∈ 𝑦)) → (𝐺‘𝐶) ⊆ (𝐺‘𝑦))
57	56	expr 461	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ ∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎))) → (𝐶 ∈ 𝑦 → (𝐺‘𝐶) ⊆ (𝐺‘𝑦)))
58		fveq2 6871	. . . . . . . . . . . 12 ⊢ (𝐶 = 𝑦 → (𝐺‘𝐶) = (𝐺‘𝑦))
59		eqimss 3997	. . . . . . . . . . . 12 ⊢ ((𝐺‘𝐶) = (𝐺‘𝑦) → (𝐺‘𝐶) ⊆ (𝐺‘𝑦))
60	58, 59	syl 18	. . . . . . . . . . 11 ⊢ (𝐶 = 𝑦 → (𝐺‘𝐶) ⊆ (𝐺‘𝑦))
61	60	a1i 11	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ ∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎))) → (𝐶 = 𝑦 → (𝐺‘𝐶) ⊆ (𝐺‘𝑦)))
62	57, 61	jaod 872	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ ∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎))) → ((𝐶 ∈ 𝑦 ∨ 𝐶 = 𝑦) → (𝐺‘𝐶) ⊆ (𝐺‘𝑦)))
63	13, 62	sylbid 243	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ ∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎))) → (𝐶 ⊆ 𝑦 → (𝐺‘𝐶) ⊆ (𝐺‘𝑦)))
64	63	ex 417	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) → (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) → (𝐶 ⊆ 𝑦 → (𝐺‘𝐶) ⊆ (𝐺‘𝑦))))
65	64	expcom 418	. . . . . 6 ⊢ (𝑦 ∈ On → ((𝜑 ∧ 𝐶 ∈ On) → (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) → (𝐶 ⊆ 𝑦 → (𝐺‘𝐶) ⊆ (𝐺‘𝑦)))))
66	65	a2d 30	. . . . 5 ⊢ (𝑦 ∈ On → (((𝜑 ∧ 𝐶 ∈ On) → ∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎))) → ((𝜑 ∧ 𝐶 ∈ On) → (𝐶 ⊆ 𝑦 → (𝐺‘𝐶) ⊆ (𝐺‘𝑦)))))
67	11, 66	biimtrid 245	. . . 4 ⊢ (𝑦 ∈ On → (∀𝑎 ∈ 𝑦 ((𝜑 ∧ 𝐶 ∈ On) → (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎))) → ((𝜑 ∧ 𝐶 ∈ On) → (𝐶 ⊆ 𝑦 → (𝐺‘𝐶) ⊆ (𝐺‘𝑦)))))
68	5, 10, 67	tfis3 7842	. . 3 ⊢ (𝐷 ∈ On → ((𝜑 ∧ 𝐶 ∈ On) → (𝐶 ⊆ 𝐷 → (𝐺‘𝐶) ⊆ (𝐺‘𝐷))))
69	68	expdcom 419	. 2 ⊢ (𝜑 → (𝐶 ∈ On → (𝐷 ∈ On → (𝐶 ⊆ 𝐷 → (𝐺‘𝐶) ⊆ (𝐺‘𝐷)))))
70	69	3imp2 1366	1 ⊢ ((𝜑 ∧ (𝐶 ∈ On ∧ 𝐷 ∈ On ∧ 𝐶 ⊆ 𝐷)) → (𝐺‘𝐶) ⊆ (𝐺‘𝐷))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   ∨ wo 860   ∧ w3a 1101  ∀wal 1561   = wceq 1563   ∈ wcel 2145  ∀wral 3079  Vcvv 3457   ∖ cdif 3904   ∪ cun 3905   ∩ cin 3906   ⊆ wss 3907  ∅c0 4288  ifcif 4483  𝒫 cpw 4558  {csn 4585  ∪ cuni 4868   ↦ cmpt 5186  dom cdm 5652  ran crn 5653   “ cima 5655  Ord word 6349  Oncon0 6350  suc csuc 6352   Fn wfn 6520  –1-1-onto→wf1o 6524  ‘cfv 6525  recscrecs 8345  Fincfn 8931  cardccrd 9909

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-rep 5232  ax-sep 5251  ax-nul 5261  ax-pr 5395  ax-un 7722

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3080  df-rex 3090  df-reu 3371  df-rab 3418  df-v 3459  df-sbc 3748  df-csb 3856  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-pss 3927  df-nul 4289  df-if 4484  df-pw 4560  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-iun 4954  df-br 5106  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5547  df-eprel 5552  df-po 5560  df-so 5561  df-fr 5605  df-we 5607  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-rn 5663  df-res 5664  df-ima 5665  df-pred 6292  df-ord 6353  df-on 6354  df-suc 6356  df-iota 6481  df-fun 6527  df-fn 6528  df-f 6529  df-f1 6530  df-fo 6531  df-f1o 6532  df-fv 6533  df-ov 7403  df-2nd 7975  df-frecs 8266  df-wrecs 8297  df-recs 8346

This theorem is referenced by:  ttukeylem6  10486  ttukeylem7  10487