Theorem ttukeylem5 10551

Description: Lemma for ttukey 10556. 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 4022	. . . . . 6 ⊢ (𝑦 = 𝑎 → (𝐶 ⊆ 𝑦 ↔ 𝐶 ⊆ 𝑎))
2		fveq2 6907	. . . . . . 7 ⊢ (𝑦 = 𝑎 → (𝐺‘𝑦) = (𝐺‘𝑎))
3	2	sseq2d 4028	. . . . . 6 ⊢ (𝑦 = 𝑎 → ((𝐺‘𝐶) ⊆ (𝐺‘𝑦) ↔ (𝐺‘𝐶) ⊆ (𝐺‘𝑎)))
4	1, 3	imbi12d 344	. . . . 5 ⊢ (𝑦 = 𝑎 → ((𝐶 ⊆ 𝑦 → (𝐺‘𝐶) ⊆ (𝐺‘𝑦)) ↔ (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎))))
5	4	imbi2d 340	. . . 4 ⊢ (𝑦 = 𝑎 → (((𝜑 ∧ 𝐶 ∈ On) → (𝐶 ⊆ 𝑦 → (𝐺‘𝐶) ⊆ (𝐺‘𝑦))) ↔ ((𝜑 ∧ 𝐶 ∈ On) → (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)))))
6		sseq2 4022	. . . . . 6 ⊢ (𝑦 = 𝐷 → (𝐶 ⊆ 𝑦 ↔ 𝐶 ⊆ 𝐷))
7		fveq2 6907	. . . . . . 7 ⊢ (𝑦 = 𝐷 → (𝐺‘𝑦) = (𝐺‘𝐷))
8	7	sseq2d 4028	. . . . . 6 ⊢ (𝑦 = 𝐷 → ((𝐺‘𝐶) ⊆ (𝐺‘𝑦) ↔ (𝐺‘𝐶) ⊆ (𝐺‘𝐷)))
9	6, 8	imbi12d 344	. . . . 5 ⊢ (𝑦 = 𝐷 → ((𝐶 ⊆ 𝑦 → (𝐺‘𝐶) ⊆ (𝐺‘𝑦)) ↔ (𝐶 ⊆ 𝐷 → (𝐺‘𝐶) ⊆ (𝐺‘𝐷))))
10	9	imbi2d 340	. . . 4 ⊢ (𝑦 = 𝐷 → (((𝜑 ∧ 𝐶 ∈ On) → (𝐶 ⊆ 𝑦 → (𝐺‘𝐶) ⊆ (𝐺‘𝑦))) ↔ ((𝜑 ∧ 𝐶 ∈ On) → (𝐶 ⊆ 𝐷 → (𝐺‘𝐶) ⊆ (𝐺‘𝐷)))))
11		r19.21v 3178	. . . . 5 ⊢ (∀𝑎 ∈ 𝑦 ((𝜑 ∧ 𝐶 ∈ On) → (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎))) ↔ ((𝜑 ∧ 𝐶 ∈ On) → ∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎))))
12		onsseleq 6427	. . . . . . . . . 10 ⊢ ((𝐶 ∈ On ∧ 𝑦 ∈ On) → (𝐶 ⊆ 𝑦 ↔ (𝐶 ∈ 𝑦 ∨ 𝐶 = 𝑦)))
13	12	ad4ant23 753	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ ∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎))) → (𝐶 ⊆ 𝑦 ↔ (𝐶 ∈ 𝑦 ∨ 𝐶 = 𝑦)))
14		sseq2 4022	. . . . . . . . . . . . 13 ⊢ (if(𝑦 = ∅, 𝐵, ∪ (𝐺 “ 𝑦)) = if(𝑦 = ∪ 𝑦, if(𝑦 = ∅, 𝐵, ∪ (𝐺 “ 𝑦)), ((𝐺‘∪ 𝑦) ∪ if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅))) → ((𝐺‘𝐶) ⊆ if(𝑦 = ∅, 𝐵, ∪ (𝐺 “ 𝑦)) ↔ (𝐺‘𝐶) ⊆ if(𝑦 = ∪ 𝑦, if(𝑦 = ∅, 𝐵, ∪ (𝐺 “ 𝑦)), ((𝐺‘∪ 𝑦) ∪ if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅)))))
15		sseq2 4022	. . . . . . . . . . . . 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 8436	. . . . . . . . . . . . . . . . 17 ⊢ 𝐺 Fn On
18		simplr 769	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ∧ 𝐶 ∈ 𝑦)) → 𝑦 ∈ On)
19		onss 7804	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ On → 𝑦 ⊆ On)
20	18, 19	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ∧ 𝐶 ∈ 𝑦)) → 𝑦 ⊆ On)
21		simprr 773	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ∧ 𝐶 ∈ 𝑦)) → 𝐶 ∈ 𝑦)
22		fnfvima 7253	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐺 Fn On ∧ 𝑦 ⊆ On ∧ 𝐶 ∈ 𝑦) → (𝐺‘𝐶) ∈ (𝐺 “ 𝑦))
23	17, 20, 21, 22	mp3an2i 1465	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ∧ 𝐶 ∈ 𝑦)) → (𝐺‘𝐶) ∈ (𝐺 “ 𝑦))
24		elssuni 4942	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺‘𝐶) ∈ (𝐺 “ 𝑦) → (𝐺‘𝐶) ⊆ ∪ (𝐺 “ 𝑦))
25	23, 24	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ∧ 𝐶 ∈ 𝑦)) → (𝐺‘𝐶) ⊆ ∪ (𝐺 “ 𝑦))
26		n0i 4346	. . . . . . . . . . . . . . . 16 ⊢ (𝐶 ∈ 𝑦 → ¬ 𝑦 = ∅)
27		iffalse 4540	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝑦 = ∅ → if(𝑦 = ∅, 𝐵, ∪ (𝐺 “ 𝑦)) = ∪ (𝐺 “ 𝑦))
28	21, 26, 27	3syl 18	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ∧ 𝐶 ∈ 𝑦)) → if(𝑦 = ∅, 𝐵, ∪ (𝐺 “ 𝑦)) = ∪ (𝐺 “ 𝑦))
29	25, 28	sseqtrrd 4037	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ∧ 𝐶 ∈ 𝑦)) → (𝐺‘𝐶) ⊆ if(𝑦 = ∅, 𝐵, ∪ (𝐺 “ 𝑦)))
30	29	adantr 480	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ∧ 𝐶 ∈ 𝑦)) ∧ 𝑦 = ∪ 𝑦) → (𝐺‘𝐶) ⊆ if(𝑦 = ∅, 𝐵, ∪ (𝐺 “ 𝑦)))
31	21	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ∧ 𝐶 ∈ 𝑦)) ∧ ¬ 𝑦 = ∪ 𝑦) → 𝐶 ∈ 𝑦)
32		elssuni 4942	. . . . . . . . . . . . . . . 16 ⊢ (𝐶 ∈ 𝑦 → 𝐶 ⊆ ∪ 𝑦)
33	31, 32	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ∧ 𝐶 ∈ 𝑦)) ∧ ¬ 𝑦 = ∪ 𝑦) → 𝐶 ⊆ ∪ 𝑦)
34		sseq2 4022	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = ∪ 𝑦 → (𝐶 ⊆ 𝑎 ↔ 𝐶 ⊆ ∪ 𝑦))
35		fveq2 6907	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑎 = ∪ 𝑦 → (𝐺‘𝑎) = (𝐺‘∪ 𝑦))
36	35	sseq2d 4028	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = ∪ 𝑦 → ((𝐺‘𝐶) ⊆ (𝐺‘𝑎) ↔ (𝐺‘𝐶) ⊆ (𝐺‘∪ 𝑦)))
37	34, 36	imbi12d 344	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = ∪ 𝑦 → ((𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ↔ (𝐶 ⊆ ∪ 𝑦 → (𝐺‘𝐶) ⊆ (𝐺‘∪ 𝑦))))
38		simplrl 777	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ∧ 𝐶 ∈ 𝑦)) ∧ ¬ 𝑦 = ∪ 𝑦) → ∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)))
39		vuniex 7758	. . . . . . . . . . . . . . . . . 18 ⊢ ∪ 𝑦 ∈ V
40	39	sucid 6468	. . . . . . . . . . . . . . . . 17 ⊢ ∪ 𝑦 ∈ suc ∪ 𝑦
41		eloni 6396	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ On → Ord 𝑦)
42		orduniorsuc 7850	. . . . . . . . . . . . . . . . . . 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 2846	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ∧ 𝐶 ∈ 𝑦)) ∧ ¬ 𝑦 = ∪ 𝑦) → ∪ 𝑦 ∈ 𝑦)
46	37, 38, 45	rspcdva 3623	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ∧ 𝐶 ∈ 𝑦)) ∧ ¬ 𝑦 = ∪ 𝑦) → (𝐶 ⊆ ∪ 𝑦 → (𝐺‘𝐶) ⊆ (𝐺‘∪ 𝑦)))
47	33, 46	mpd 15	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ∧ 𝐶 ∈ 𝑦)) ∧ ¬ 𝑦 = ∪ 𝑦) → (𝐺‘𝐶) ⊆ (𝐺‘∪ 𝑦))
48		ssun1 4188	. . . . . . . . . . . . . 14 ⊢ (𝐺‘∪ 𝑦) ⊆ ((𝐺‘∪ 𝑦) ∪ if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅))
49	47, 48	sstrdi 4008	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ∧ 𝐶 ∈ 𝑦)) ∧ ¬ 𝑦 = ∪ 𝑦) → (𝐺‘𝐶) ⊆ ((𝐺‘∪ 𝑦) ∪ if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅)))
50	14, 15, 30, 49	ifbothda 4569	. . . . . . . . . . . 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 10549	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ On) → (𝐺‘𝑦) = if(𝑦 = ∪ 𝑦, if(𝑦 = ∅, 𝐵, ∪ (𝐺 “ 𝑦)), ((𝐺‘∪ 𝑦) ∪ if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅))))
55	54	ad4ant13 751	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ∧ 𝐶 ∈ 𝑦)) → (𝐺‘𝑦) = if(𝑦 = ∪ 𝑦, if(𝑦 = ∅, 𝐵, ∪ (𝐺 “ 𝑦)), ((𝐺‘∪ 𝑦) ∪ if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅))))
56	50, 55	sseqtrrd 4037	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ (∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎)) ∧ 𝐶 ∈ 𝑦)) → (𝐺‘𝐶) ⊆ (𝐺‘𝑦))
57	56	expr 456	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝐶 ∈ On) ∧ 𝑦 ∈ On) ∧ ∀𝑎 ∈ 𝑦 (𝐶 ⊆ 𝑎 → (𝐺‘𝐶) ⊆ (𝐺‘𝑎))) → (𝐶 ∈ 𝑦 → (𝐺‘𝐶) ⊆ (𝐺‘𝑦)))
58		fveq2 6907	. . . . . . . . . . . 12 ⊢ (𝐶 = 𝑦 → (𝐺‘𝐶) = (𝐺‘𝑦))
59		eqimss 4054	. . . . . . . . . . . 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 7879	. . 3 ⊢ (𝐷 ∈ On → ((𝜑 ∧ 𝐶 ∈ On) → (𝐶 ⊆ 𝐷 → (𝐺‘𝐶) ⊆ (𝐺‘𝐷))))
69	68	expdcom 414	. 2 ⊢ (𝜑 → (𝐶 ∈ On → (𝐷 ∈ On → (𝐶 ⊆ 𝐷 → (𝐺‘𝐶) ⊆ (𝐺‘𝐷)))))
70	69	3imp2 1348	1 ⊢ ((𝜑 ∧ (𝐶 ∈ On ∧ 𝐷 ∈ On ∧ 𝐶 ⊆ 𝐷)) → (𝐺‘𝐶) ⊆ (𝐺‘𝐷))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847   ∧ w3a 1086  ∀wal 1535   = wceq 1537   ∈ wcel 2106  ∀wral 3059  Vcvv 3478   ∖ cdif 3960   ∪ cun 3961   ∩ cin 3962   ⊆ wss 3963  ∅c0 4339  ifcif 4531  𝒫 cpw 4605  {csn 4631  ∪ cuni 4912   ↦ cmpt 5231  dom cdm 5689  ran crn 5690   “ cima 5692  Ord word 6385  Oncon0 6386  suc csuc 6388   Fn wfn 6558  –1-1-onto→wf1o 6562  ‘cfv 6563  recscrecs 8409  Fincfn 8984  cardccrd 9973

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-rep 5285  ax-sep 5302  ax-nul 5312  ax-pr 5438  ax-un 7754

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-ral 3060  df-rex 3069  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-pss 3983  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5583  df-eprel 5589  df-po 5597  df-so 5598  df-fr 5641  df-we 5643  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-pred 6323  df-ord 6389  df-on 6390  df-suc 6392  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-ov 7434  df-2nd 8014  df-frecs 8305  df-wrecs 8336  df-recs 8410

This theorem is referenced by:  ttukeylem6  10552  ttukeylem7  10553