Theorem ttukeylem5 10449

Description: Lemma for ttukey 10454. 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 3970	. . . . . 6 ⊢ (𝑦 = 𝑎 → (𝐶 ⊆ 𝑦 ↔ 𝐶 ⊆ 𝑎))
2		fveq2 6842	. . . . . . 7 ⊢ (𝑦 = 𝑎 → (𝐺‘𝑦) = (𝐺‘𝑎))
3	2	sseq2d 3976	. . . . . 6 ⊢ (𝑦 = 𝑎 → ((𝐺‘𝐶) ⊆ (𝐺‘𝑦) ↔ (𝐺‘𝐶) ⊆ (𝐺‘𝑎)))
4	1, 3	imbi12d 344	. . . . 5 ⊢ (𝑦 = 𝑎 → ((𝐶 ⊆ 𝑦 → (𝐺‘𝐶) ⊆ (𝐺‘𝑦)) ↔ (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎))))
5	4	imbi2d 340	. . . 4 ⊢ (𝑦 = 𝑎 → (((𝜑 ∧ 𝐶 ∈ On) → (𝐶 ⊆ 𝑦 → (𝐺‘𝐶) ⊆ (𝐺‘𝑦))) ↔ ((𝜑 ∧ 𝐶 ∈ On) → (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)))))
6		sseq2 3970	. . . . . 6 ⊢ (𝑦 = 𝐷 → (𝐶 ⊆ 𝑦 ↔ 𝐶 ⊆ 𝐷))
7		fveq2 6842	. . . . . . 7 ⊢ (𝑦 = 𝐷 → (𝐺‘𝑦) = (𝐺‘𝐷))
8	7	sseq2d 3976	. . . . . 6 ⊢ (𝑦 = 𝐷 → ((𝐺‘𝐶) ⊆ (𝐺‘𝑦) ↔ (𝐺‘𝐶) ⊆ (𝐺‘𝐷)))
9	6, 8	imbi12d 344	. . . . 5 ⊢ (𝑦 = 𝐷 → ((𝐶 ⊆ 𝑦 → (𝐺‘𝐶) ⊆ (𝐺‘𝑦)) ↔ (𝐶 ⊆ 𝐷 → (𝐺‘𝐶) ⊆ (𝐺‘𝐷))))
10	9	imbi2d 340	. . . 4 ⊢ (𝑦 = 𝐷 → (((𝜑 ∧ 𝐶 ∈ On) → (𝐶 ⊆ 𝑦 → (𝐺‘𝐶) ⊆ (𝐺‘𝑦))) ↔ ((𝜑 ∧ 𝐶 ∈ On) → (𝐶 ⊆ 𝐷 → (𝐺‘𝐶) ⊆ (𝐺‘𝐷)))))
11		r19.21v 3176	. . . . 5 ⊢ (∀𝑎 ∈ 𝑦 ((𝜑 ∧ 𝐶 ∈ On) → (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎))) ↔ ((𝜑 ∧ 𝐶 ∈ On) → ∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎))))
12		onsseleq 6358	. . . . . . . . . 10 ⊢ ((𝐶 ∈ On ∧ 𝑦 ∈ On) → (𝐶 ⊆ 𝑦 ↔ (𝐶 ∈ 𝑦 ∨ 𝐶 = 𝑦)))
13	12	ad4ant23 751	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ ∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎))) → (𝐶 ⊆ 𝑦 ↔ (𝐶 ∈ 𝑦 ∨ 𝐶 = 𝑦)))
14		sseq2 3970	. . . . . . . . . . . . 13 ⊢ (if(𝑦 = ∅, 𝐵, ∪ (𝐺 “ 𝑦)) = if(𝑦 = ∪ 𝑦, if(𝑦 = ∅, 𝐵, ∪ (𝐺 “ 𝑦)), ((𝐺‘∪ 𝑦) ∪ if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅))) → ((𝐺‘𝐶) ⊆ if(𝑦 = ∅, 𝐵, ∪ (𝐺 “ 𝑦)) ↔ (𝐺‘𝐶) ⊆ if(𝑦 = ∪ 𝑦, if(𝑦 = ∅, 𝐵, ∪ (𝐺 “ 𝑦)), ((𝐺‘∪ 𝑦) ∪ if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅)))))
15		sseq2 3970	. . . . . . . . . . . . 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 8343	. . . . . . . . . . . . . . . . 17 ⊢ 𝐺 Fn On
18		simplr 767	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ∧ 𝐶 ∈ 𝑦)) → 𝑦 ∈ On)
19		onss 7719	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ On → 𝑦 ⊆ On)
20	18, 19	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ∧ 𝐶 ∈ 𝑦)) → 𝑦 ⊆ On)
21		simprr 771	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ∧ 𝐶 ∈ 𝑦)) → 𝐶 ∈ 𝑦)
22		fnfvima 7183	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐺 Fn On ∧ 𝑦 ⊆ On ∧ 𝐶 ∈ 𝑦) → (𝐺‘𝐶) ∈ (𝐺 “ 𝑦))
23	17, 20, 21, 22	mp3an2i 1466	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ∧ 𝐶 ∈ 𝑦)) → (𝐺‘𝐶) ∈ (𝐺 “ 𝑦))
24		elssuni 4898	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺‘𝐶) ∈ (𝐺 “ 𝑦) → (𝐺‘𝐶) ⊆ ∪ (𝐺 “ 𝑦))
25	23, 24	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ∧ 𝐶 ∈ 𝑦)) → (𝐺‘𝐶) ⊆ ∪ (𝐺 “ 𝑦))
26		n0i 4293	. . . . . . . . . . . . . . . 16 ⊢ (𝐶 ∈ 𝑦 → ¬ 𝑦 = ∅)
27		iffalse 4495	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝑦 = ∅ → if(𝑦 = ∅, 𝐵, ∪ (𝐺 “ 𝑦)) = ∪ (𝐺 “ 𝑦))
28	21, 26, 27	3syl 18	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ∧ 𝐶 ∈ 𝑦)) → if(𝑦 = ∅, 𝐵, ∪ (𝐺 “ 𝑦)) = ∪ (𝐺 “ 𝑦))
29	25, 28	sseqtrrd 3985	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ∧ 𝐶 ∈ 𝑦)) → (𝐺‘𝐶) ⊆ if(𝑦 = ∅, 𝐵, ∪ (𝐺 “ 𝑦)))
30	29	adantr 481	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ∧ 𝐶 ∈ 𝑦)) ∧ 𝑦 = ∪ 𝑦) → (𝐺‘𝐶) ⊆ if(𝑦 = ∅, 𝐵, ∪ (𝐺 “ 𝑦)))
31	21	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ∧ 𝐶 ∈ 𝑦)) ∧ ¬ 𝑦 = ∪ 𝑦) → 𝐶 ∈ 𝑦)
32		elssuni 4898	. . . . . . . . . . . . . . . 16 ⊢ (𝐶 ∈ 𝑦 → 𝐶 ⊆ ∪ 𝑦)
33	31, 32	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ∧ 𝐶 ∈ 𝑦)) ∧ ¬ 𝑦 = ∪ 𝑦) → 𝐶 ⊆ ∪ 𝑦)
34		sseq2 3970	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = ∪ 𝑦 → (𝐶 ⊆ 𝑎 ↔ 𝐶 ⊆ ∪ 𝑦))
35		fveq2 6842	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = ∪ 𝑦 → (𝐺‘𝑎) = (𝐺‘∪ 𝑦))
36	35	sseq2d 3976	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = ∪ 𝑦 → ((𝐺‘𝐶) ⊆ (𝐺‘𝑎) ↔ (𝐺‘𝐶) ⊆ (𝐺‘∪ 𝑦)))
37	34, 36	imbi12d 344	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = ∪ 𝑦 → ((𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ↔ (𝐶 ⊆ ∪ 𝑦 → (𝐺‘𝐶) ⊆ (𝐺‘∪ 𝑦))))
38		simplrl 775	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ∧ 𝐶 ∈ 𝑦)) ∧ ¬ 𝑦 = ∪ 𝑦) → ∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)))
39		vuniex 7676	. . . . . . . . . . . . . . . . . 18 ⊢ ∪ 𝑦 ∈ V
40	39	sucid 6399	. . . . . . . . . . . . . . . . 17 ⊢ ∪ 𝑦 ∈ suc ∪ 𝑦
41		eloni 6327	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ On → Ord 𝑦)
42		orduniorsuc 7765	. . . . . . . . . . . . . . . . . . 19 ⊢ (Ord 𝑦 → (𝑦 = ∪ 𝑦 ∨ 𝑦 = suc ∪ 𝑦))
43	18, 41, 42	3syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ∧ 𝐶 ∈ 𝑦)) → (𝑦 = ∪ 𝑦 ∨ 𝑦 = suc ∪ 𝑦))
44	43	orcanai 1001	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ∧ 𝐶 ∈ 𝑦)) ∧ ¬ 𝑦 = ∪ 𝑦) → 𝑦 = suc ∪ 𝑦)
45	40, 44	eleqtrrid 2845	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ∧ 𝐶 ∈ 𝑦)) ∧ ¬ 𝑦 = ∪ 𝑦) → ∪ 𝑦 ∈ 𝑦)
46	37, 38, 45	rspcdva 3582	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ∧ 𝐶 ∈ 𝑦)) ∧ ¬ 𝑦 = ∪ 𝑦) → (𝐶 ⊆ ∪ 𝑦 → (𝐺‘𝐶) ⊆ (𝐺‘∪ 𝑦)))
47	33, 46	mpd 15	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ∧ 𝐶 ∈ 𝑦)) ∧ ¬ 𝑦 = ∪ 𝑦) → (𝐺‘𝐶) ⊆ (𝐺‘∪ 𝑦))
48		ssun1 4132	. . . . . . . . . . . . . 14 ⊢ (𝐺‘∪ 𝑦) ⊆ ((𝐺‘∪ 𝑦) ∪ if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅))
49	47, 48	sstrdi 3956	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ∧ 𝐶 ∈ 𝑦)) ∧ ¬ 𝑦 = ∪ 𝑦) → (𝐺‘𝐶) ⊆ ((𝐺‘∪ 𝑦) ∪ if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅)))
50	14, 15, 30, 49	ifbothda 4524	. . . . . . . . . . . 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 10447	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ On) → (𝐺‘𝑦) = if(𝑦 = ∪ 𝑦, if(𝑦 = ∅, 𝐵, ∪ (𝐺 “ 𝑦)), ((𝐺‘∪ 𝑦) ∪ if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅))))
55	54	ad4ant13 749	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ∧ 𝐶 ∈ 𝑦)) → (𝐺‘𝑦) = if(𝑦 = ∪ 𝑦, if(𝑦 = ∅, 𝐵, ∪ (𝐺 “ 𝑦)), ((𝐺‘∪ 𝑦) ∪ if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅))))
56	50, 55	sseqtrrd 3985	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ∧ 𝐶 ∈ 𝑦)) → (𝐺‘𝐶) ⊆ (𝐺‘𝑦))
57	56	expr 457	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ ∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎))) → (𝐶 ∈ 𝑦 → (𝐺‘𝐶) ⊆ (𝐺‘𝑦)))
58		fveq2 6842	. . . . . . . . . . . 12 ⊢ (𝐶 = 𝑦 → (𝐺‘𝐶) = (𝐺‘𝑦))
59		eqimss 4000	. . . . . . . . . . . 12 ⊢ ((𝐺‘𝐶) = (𝐺‘𝑦) → (𝐺‘𝐶) ⊆ (𝐺‘𝑦))
60	58, 59	syl 17	. . . . . . . . . . 11 ⊢ (𝐶 = 𝑦 → (𝐺‘𝐶) ⊆ (𝐺‘𝑦))
61	60	a1i 11	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ ∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎))) → (𝐶 = 𝑦 → (𝐺‘𝐶) ⊆ (𝐺‘𝑦)))
62	57, 61	jaod 857	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ ∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎))) → ((𝐶 ∈ 𝑦 ∨ 𝐶 = 𝑦) → (𝐺‘𝐶) ⊆ (𝐺‘𝑦)))
63	13, 62	sylbid 239	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ ∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎))) → (𝐶 ⊆ 𝑦 → (𝐺‘𝐶) ⊆ (𝐺‘𝑦)))
64	63	ex 413	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) → (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) → (𝐶 ⊆ 𝑦 → (𝐺‘𝐶) ⊆ (𝐺‘𝑦))))
65	64	expcom 414	. . . . . 6 ⊢ (𝑦 ∈ On → ((𝜑 ∧ 𝐶 ∈ On) → (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) → (𝐶 ⊆ 𝑦 → (𝐺‘𝐶) ⊆ (𝐺‘𝑦)))))
66	65	a2d 29	. . . . 5 ⊢ (𝑦 ∈ On → (((𝜑 ∧ 𝐶 ∈ On) → ∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎))) → ((𝜑 ∧ 𝐶 ∈ On) → (𝐶 ⊆ 𝑦 → (𝐺‘𝐶) ⊆ (𝐺‘𝑦)))))
67	11, 66	biimtrid 241	. . . 4 ⊢ (𝑦 ∈ On → (∀𝑎 ∈ 𝑦 ((𝜑 ∧ 𝐶 ∈ On) → (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎))) → ((𝜑 ∧ 𝐶 ∈ On) → (𝐶 ⊆ 𝑦 → (𝐺‘𝐶) ⊆ (𝐺‘𝑦)))))
68	5, 10, 67	tfis3 7794	. . 3 ⊢ (𝐷 ∈ On → ((𝜑 ∧ 𝐶 ∈ On) → (𝐶 ⊆ 𝐷 → (𝐺‘𝐶) ⊆ (𝐺‘𝐷))))
69	68	expdcom 415	. 2 ⊢ (𝜑 → (𝐶 ∈ On → (𝐷 ∈ On → (𝐶 ⊆ 𝐷 → (𝐺‘𝐶) ⊆ (𝐺‘𝐷)))))
70	69	3imp2 1349	1 ⊢ ((𝜑 ∧ (𝐶 ∈ On ∧ 𝐷 ∈ On ∧ 𝐶 ⊆ 𝐷)) → (𝐺‘𝐶) ⊆ (𝐺‘𝐷))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   ∨ wo 845   ∧ w3a 1087  ∀wal 1539   = wceq 1541   ∈ wcel 2106  ∀wral 3064  Vcvv 3445   ∖ cdif 3907   ∪ cun 3908   ∩ cin 3909   ⊆ wss 3910  ∅c0 4282  ifcif 4486  𝒫 cpw 4560  {csn 4586  ∪ cuni 4865   ↦ cmpt 5188  dom cdm 5633  ran crn 5634   “ cima 5636  Ord word 6316  Oncon0 6317  suc csuc 6319   Fn wfn 6491  –1-1-onto→wf1o 6495  ‘cfv 6496  recscrecs 8316  Fincfn 8883  cardccrd 9871

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pr 5384  ax-un 7672

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-ov 7360  df-2nd 7922  df-frecs 8212  df-wrecs 8243  df-recs 8317

This theorem is referenced by:  ttukeylem6  10450  ttukeylem7  10451