Theorem ttukeylem6 10528

Description: Lemma for ttukey 10532. (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
ttukeylem6	⊢ ((𝜑 ∧ 𝐶 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵))) → (𝐺‘𝐶) ∈ 𝐴)

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

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem ttukeylem6

Dummy variables 𝑎 𝑦 𝑓 𝑢 𝑣 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		cardon 9958	. . . . 5 ⊢ (card‘(∪ 𝐴 ∖ 𝐵)) ∈ On
2	1	onsuci 7833	. . . 4 ⊢ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∈ On
3	2	a1i 11	. . 3 ⊢ (𝜑 → suc (card‘(∪ 𝐴 ∖ 𝐵)) ∈ On)
4		onelon 6377	. . 3 ⊢ ((suc (card‘(∪ 𝐴 ∖ 𝐵)) ∈ On ∧ 𝐶 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵))) → 𝐶 ∈ On)
5	3, 4	sylan 580	. 2 ⊢ ((𝜑 ∧ 𝐶 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵))) → 𝐶 ∈ On)
6		eleq1 2822	. . . . . 6 ⊢ (𝑦 = 𝑎 → (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ↔ 𝑎 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵))))
7		fveq2 6876	. . . . . . 7 ⊢ (𝑦 = 𝑎 → (𝐺‘𝑦) = (𝐺‘𝑎))
8	7	eleq1d 2819	. . . . . 6 ⊢ (𝑦 = 𝑎 → ((𝐺‘𝑦) ∈ 𝐴 ↔ (𝐺‘𝑎) ∈ 𝐴))
9	6, 8	imbi12d 344	. . . . 5 ⊢ (𝑦 = 𝑎 → ((𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → (𝐺‘𝑦) ∈ 𝐴) ↔ (𝑎 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → (𝐺‘𝑎) ∈ 𝐴)))
10	9	imbi2d 340	. . . 4 ⊢ (𝑦 = 𝑎 → ((𝜑 → (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → (𝐺‘𝑦) ∈ 𝐴)) ↔ (𝜑 → (𝑎 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → (𝐺‘𝑎) ∈ 𝐴))))
11		eleq1 2822	. . . . . 6 ⊢ (𝑦 = 𝐶 → (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ↔ 𝐶 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵))))
12		fveq2 6876	. . . . . . 7 ⊢ (𝑦 = 𝐶 → (𝐺‘𝑦) = (𝐺‘𝐶))
13	12	eleq1d 2819	. . . . . 6 ⊢ (𝑦 = 𝐶 → ((𝐺‘𝑦) ∈ 𝐴 ↔ (𝐺‘𝐶) ∈ 𝐴))
14	11, 13	imbi12d 344	. . . . 5 ⊢ (𝑦 = 𝐶 → ((𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → (𝐺‘𝑦) ∈ 𝐴) ↔ (𝐶 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → (𝐺‘𝐶) ∈ 𝐴)))
15	14	imbi2d 340	. . . 4 ⊢ (𝑦 = 𝐶 → ((𝜑 → (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → (𝐺‘𝑦) ∈ 𝐴)) ↔ (𝜑 → (𝐶 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → (𝐺‘𝐶) ∈ 𝐴))))
16		r19.21v 3165	. . . . . 6 ⊢ (∀𝑎 ∈ 𝑦 (𝜑 → (𝑎 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → (𝐺‘𝑎) ∈ 𝐴)) ↔ (𝜑 → ∀𝑎 ∈ 𝑦 (𝑎 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → (𝐺‘𝑎) ∈ 𝐴)))
17	2	onordi 6465	. . . . . . . . . . . . . . 15 ⊢ Ord suc (card‘(∪ 𝐴 ∖ 𝐵))
18	17	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → Ord suc (card‘(∪ 𝐴 ∖ 𝐵)))
19		ordelss 6368	. . . . . . . . . . . . . 14 ⊢ ((Ord suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ 𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵))) → 𝑦 ⊆ suc (card‘(∪ 𝐴 ∖ 𝐵)))
20	18, 19	sylan 580	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵))) → 𝑦 ⊆ suc (card‘(∪ 𝐴 ∖ 𝐵)))
21	20	sselda 3958	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵))) ∧ 𝑎 ∈ 𝑦) → 𝑎 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)))
22		biimt 360	. . . . . . . . . . . 12 ⊢ (𝑎 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → ((𝐺‘𝑎) ∈ 𝐴 ↔ (𝑎 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → (𝐺‘𝑎) ∈ 𝐴)))
23	21, 22	syl 17	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵))) ∧ 𝑎 ∈ 𝑦) → ((𝐺‘𝑎) ∈ 𝐴 ↔ (𝑎 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → (𝐺‘𝑎) ∈ 𝐴)))
24	23	ralbidva 3161	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵))) → (∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴 ↔ ∀𝑎 ∈ 𝑦 (𝑎 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → (𝐺‘𝑎) ∈ 𝐴)))
25	2	onssi 7832	. . . . . . . . . . . . . 14 ⊢ suc (card‘(∪ 𝐴 ∖ 𝐵)) ⊆ On
26		simprl 770	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) → 𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)))
27	25, 26	sselid 3956	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) → 𝑦 ∈ On)
28		ttukeylem.1	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐹:(card‘(∪ 𝐴 ∖ 𝐵))–1-1-onto→(∪ 𝐴 ∖ 𝐵))
29		ttukeylem.2	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐵 ∈ 𝐴)
30		ttukeylem.3	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 ↔ (𝒫 𝑥 ∩ Fin) ⊆ 𝐴))
31		ttukeylem.4	. . . . . . . . . . . . . 14 ⊢ 𝐺 = recs((𝑧 ∈ V ↦ if(dom 𝑧 = ∪ dom 𝑧, if(dom 𝑧 = ∅, 𝐵, ∪ ran 𝑧), ((𝑧‘∪ dom 𝑧) ∪ if(((𝑧‘∪ dom 𝑧) ∪ {(𝐹‘∪ dom 𝑧)}) ∈ 𝐴, {(𝐹‘∪ dom 𝑧)}, ∅)))))
32	28, 29, 30, 31	ttukeylem3 10525	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ On) → (𝐺‘𝑦) = if(𝑦 = ∪ 𝑦, if(𝑦 = ∅, 𝐵, ∪ (𝐺 “ 𝑦)), ((𝐺‘∪ 𝑦) ∪ if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅))))
33	27, 32	syldan 591	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) → (𝐺‘𝑦) = if(𝑦 = ∪ 𝑦, if(𝑦 = ∅, 𝐵, ∪ (𝐺 “ 𝑦)), ((𝐺‘∪ 𝑦) ∪ if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅))))
34	29	ad3antrrr 730	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑦 = ∅) → 𝐵 ∈ 𝐴)
35		simpr 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) → 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin))
36	35	elin2d 4180	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) → 𝑤 ∈ Fin)
37	35	elin1d 4179	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) → 𝑤 ∈ 𝒫 ∪ (𝐺 “ 𝑦))
38	37	elpwid 4584	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) → 𝑤 ⊆ ∪ (𝐺 “ 𝑦))
39	31	tfr1 8411	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝐺 Fn On
40		fnfun 6638	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐺 Fn On → Fun 𝐺)
41		funiunfv 7240	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (Fun 𝐺 → ∪ 𝑣 ∈ 𝑦 (𝐺‘𝑣) = ∪ (𝐺 “ 𝑦))
42	39, 40, 41	mp2b 10	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ∪ 𝑣 ∈ 𝑦 (𝐺‘𝑣) = ∪ (𝐺 “ 𝑦)
43	38, 42	sseqtrrdi 4000	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) → 𝑤 ⊆ ∪ 𝑣 ∈ 𝑦 (𝐺‘𝑣))
44		dfss3 3947	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 ⊆ ∪ 𝑣 ∈ 𝑦 (𝐺‘𝑣) ↔ ∀𝑢 ∈ 𝑤 𝑢 ∈ ∪ 𝑣 ∈ 𝑦 (𝐺‘𝑣))
45		eliun 4971	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑢 ∈ ∪ 𝑣 ∈ 𝑦 (𝐺‘𝑣) ↔ ∃𝑣 ∈ 𝑦 𝑢 ∈ (𝐺‘𝑣))
46	45	ralbii 3082	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∀𝑢 ∈ 𝑤 𝑢 ∈ ∪ 𝑣 ∈ 𝑦 (𝐺‘𝑣) ↔ ∀𝑢 ∈ 𝑤 ∃𝑣 ∈ 𝑦 𝑢 ∈ (𝐺‘𝑣))
47	44, 46	bitri 275	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 ⊆ ∪ 𝑣 ∈ 𝑦 (𝐺‘𝑣) ↔ ∀𝑢 ∈ 𝑤 ∃𝑣 ∈ 𝑦 𝑢 ∈ (𝐺‘𝑣))
48	43, 47	sylib 218	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) → ∀𝑢 ∈ 𝑤 ∃𝑣 ∈ 𝑦 𝑢 ∈ (𝐺‘𝑣))
49		fveq2 6876	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑣 = (𝑓‘𝑢) → (𝐺‘𝑣) = (𝐺‘(𝑓‘𝑢)))
50	49	eleq2d 2820	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 = (𝑓‘𝑢) → (𝑢 ∈ (𝐺‘𝑣) ↔ 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))
51	50	ac6sfi 9292	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑤 ∈ Fin ∧ ∀𝑢 ∈ 𝑤 ∃𝑣 ∈ 𝑦 𝑢 ∈ (𝐺‘𝑣)) → ∃𝑓(𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))
52	36, 48, 51	syl2anc 584	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) → ∃𝑓(𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))
53		eleq1 2822	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 = ∅ → (𝑤 ∈ 𝐴 ↔ ∅ ∈ 𝐴))
54		simp-4l 782	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → 𝜑)
55		fveq2 6876	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑎 = ∪ ran 𝑓 → (𝐺‘𝑎) = (𝐺‘∪ ran 𝑓))
56	55	eleq1d 2819	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑎 = ∪ ran 𝑓 → ((𝐺‘𝑎) ∈ 𝐴 ↔ (𝐺‘∪ ran 𝑓) ∈ 𝐴))
57		simplrr 777	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) → ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)
58	57	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)
59		simprrl 780	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) → 𝑓:𝑤⟶𝑦)
60	59	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → 𝑓:𝑤⟶𝑦)
61		frn 6713	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑓:𝑤⟶𝑦 → ran 𝑓 ⊆ 𝑦)
62	60, 61	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → ran 𝑓 ⊆ 𝑦)
63	27	ad3antrrr 730	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → 𝑦 ∈ On)
64		onss 7779	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑦 ∈ On → 𝑦 ⊆ On)
65	63, 64	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → 𝑦 ⊆ On)
66	62, 65	sstrd 3969	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → ran 𝑓 ⊆ On)
67	36	adantrr 717	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) → 𝑤 ∈ Fin)
68	67	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → 𝑤 ∈ Fin)
69		ffn 6706	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑓:𝑤⟶𝑦 → 𝑓 Fn 𝑤)
70	60, 69	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → 𝑓 Fn 𝑤)
71		dffn4 6796	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑓 Fn 𝑤 ↔ 𝑓:𝑤–onto→ran 𝑓)
72	70, 71	sylib 218	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → 𝑓:𝑤–onto→ran 𝑓)
73		fofi 9323	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑤 ∈ Fin ∧ 𝑓:𝑤–onto→ran 𝑓) → ran 𝑓 ∈ Fin)
74	68, 72, 73	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → ran 𝑓 ∈ Fin)
75		dm0rn0 5904	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (dom 𝑓 = ∅ ↔ ran 𝑓 = ∅)
76	59	fdmd 6716	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) → dom 𝑓 = 𝑤)
77	76	eqeq1d 2737	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) → (dom 𝑓 = ∅ ↔ 𝑤 = ∅))
78	75, 77	bitr3id 285	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) → (ran 𝑓 = ∅ ↔ 𝑤 = ∅))
79	78	necon3bid 2976	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) → (ran 𝑓 ≠ ∅ ↔ 𝑤 ≠ ∅))
80	79	biimpar 477	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → ran 𝑓 ≠ ∅)
81		ordunifi 9298	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((ran 𝑓 ⊆ On ∧ ran 𝑓 ∈ Fin ∧ ran 𝑓 ≠ ∅) → ∪ ran 𝑓 ∈ ran 𝑓)
82	66, 74, 80, 81	syl3anc 1373	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → ∪ ran 𝑓 ∈ ran 𝑓)
83	62, 82	sseldd 3959	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → ∪ ran 𝑓 ∈ 𝑦)
84	56, 58, 83	rspcdva 3602	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → (𝐺‘∪ ran 𝑓) ∈ 𝐴)
85		simp-4l 782	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) ∧ (𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤)) → 𝜑)
86	27	ad3antrrr 730	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) ∧ (𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤)) → 𝑦 ∈ On)
87	86, 64	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) ∧ (𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤)) → 𝑦 ⊆ On)
88		ffvelcdm 7071	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤) → (𝑓‘𝑢) ∈ 𝑦)
89	88	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) ∧ (𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤)) → (𝑓‘𝑢) ∈ 𝑦)
90	87, 89	sseldd 3959	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) ∧ (𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤)) → (𝑓‘𝑢) ∈ On)
91	61	ad2antrl 728	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) ∧ (𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤)) → ran 𝑓 ⊆ 𝑦)
92	91, 87	sstrd 3969	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) ∧ (𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤)) → ran 𝑓 ⊆ On)
93		vex 3463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ 𝑓 ∈ V
94	93	rnex 7906	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ran 𝑓 ∈ V
95	94	ssonunii 7775	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (ran 𝑓 ⊆ On → ∪ ran 𝑓 ∈ On)
96	92, 95	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) ∧ (𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤)) → ∪ ran 𝑓 ∈ On)
97	69	ad2antrl 728	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) ∧ (𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤)) → 𝑓 Fn 𝑤)
98		simprr 772	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) ∧ (𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤)) → 𝑢 ∈ 𝑤)
99		fnfvelrn 7070	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑓 Fn 𝑤 ∧ 𝑢 ∈ 𝑤) → (𝑓‘𝑢) ∈ ran 𝑓)
100	97, 98, 99	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) ∧ (𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤)) → (𝑓‘𝑢) ∈ ran 𝑓)
101		elssuni 4913	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑓‘𝑢) ∈ ran 𝑓 → (𝑓‘𝑢) ⊆ ∪ ran 𝑓)
102	100, 101	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) ∧ (𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤)) → (𝑓‘𝑢) ⊆ ∪ ran 𝑓)
103	28, 29, 30, 31	ttukeylem5 10527	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ ((𝑓‘𝑢) ∈ On ∧ ∪ ran 𝑓 ∈ On ∧ (𝑓‘𝑢) ⊆ ∪ ran 𝑓)) → (𝐺‘(𝑓‘𝑢)) ⊆ (𝐺‘∪ ran 𝑓))
104	85, 90, 96, 102, 103	syl13anc 1374	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) ∧ (𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤)) → (𝐺‘(𝑓‘𝑢)) ⊆ (𝐺‘∪ ran 𝑓))
105	104	sseld 3957	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) ∧ (𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤)) → (𝑢 ∈ (𝐺‘(𝑓‘𝑢)) → 𝑢 ∈ (𝐺‘∪ ran 𝑓)))
106	105	anassrs 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) ∧ 𝑓:𝑤⟶𝑦) ∧ 𝑢 ∈ 𝑤) → (𝑢 ∈ (𝐺‘(𝑓‘𝑢)) → 𝑢 ∈ (𝐺‘∪ ran 𝑓)))
107	106	ralimdva 3152	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) ∧ 𝑓:𝑤⟶𝑦) → (∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢)) → ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘∪ ran 𝑓)))
108	107	expimpd 453	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) → ((𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))) → ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘∪ ran 𝑓)))
109	108	impr 454	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) → ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘∪ ran 𝑓))
110	109	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘∪ ran 𝑓))
111		dfss3 3947	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑤 ⊆ (𝐺‘∪ ran 𝑓) ↔ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘∪ ran 𝑓))
112	110, 111	sylibr 234	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → 𝑤 ⊆ (𝐺‘∪ ran 𝑓))
113	28, 29, 30	ttukeylem2 10524	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ ((𝐺‘∪ ran 𝑓) ∈ 𝐴 ∧ 𝑤 ⊆ (𝐺‘∪ ran 𝑓))) → 𝑤 ∈ 𝐴)
114	54, 84, 112, 113	syl12anc 836	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → 𝑤 ∈ 𝐴)
115		0ss 4375	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ∅ ⊆ 𝐵
116	28, 29, 30	ttukeylem2 10524	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝐵 ∈ 𝐴 ∧ ∅ ⊆ 𝐵)) → ∅ ∈ 𝐴)
117	115, 116	mpanr2 704	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝐵 ∈ 𝐴) → ∅ ∈ 𝐴)
118	29, 117	mpdan 687	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ∅ ∈ 𝐴)
119	118	ad3antrrr 730	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) → ∅ ∈ 𝐴)
120	53, 114, 119	pm2.61ne 3017	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) → 𝑤 ∈ 𝐴)
121	120	expr 456	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) → ((𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))) → 𝑤 ∈ 𝐴))
122	121	exlimdv 1933	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) → (∃𝑓(𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))) → 𝑤 ∈ 𝐴))
123	52, 122	mpd 15	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) → 𝑤 ∈ 𝐴)
124	123	ex 412	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) → (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) → 𝑤 ∈ 𝐴))
125	124	ssrdv 3964	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) → (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ⊆ 𝐴)
126	28, 29, 30	ttukeylem1 10523	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (∪ (𝐺 “ 𝑦) ∈ 𝐴 ↔ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ⊆ 𝐴))
127	126	ad2antrr 726	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) → (∪ (𝐺 “ 𝑦) ∈ 𝐴 ↔ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ⊆ 𝐴))
128	125, 127	mpbird 257	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) → ∪ (𝐺 “ 𝑦) ∈ 𝐴)
129	128	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ ¬ 𝑦 = ∅) → ∪ (𝐺 “ 𝑦) ∈ 𝐴)
130	34, 129	ifclda 4536	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) → if(𝑦 = ∅, 𝐵, ∪ (𝐺 “ 𝑦)) ∈ 𝐴)
131		uneq2 4137	. . . . . . . . . . . . . . 15 ⊢ ({(𝐹‘∪ 𝑦)} = if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅) → ((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) = ((𝐺‘∪ 𝑦) ∪ if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅)))
132	131	eleq1d 2819	. . . . . . . . . . . . . 14 ⊢ ({(𝐹‘∪ 𝑦)} = if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅) → (((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴 ↔ ((𝐺‘∪ 𝑦) ∪ if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅)) ∈ 𝐴))
133		un0 4369	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺‘∪ 𝑦) ∪ ∅) = (𝐺‘∪ 𝑦)
134		uneq2 4137	. . . . . . . . . . . . . . . 16 ⊢ (∅ = if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅) → ((𝐺‘∪ 𝑦) ∪ ∅) = ((𝐺‘∪ 𝑦) ∪ if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅)))
135	133, 134	eqtr3id 2784	. . . . . . . . . . . . . . 15 ⊢ (∅ = if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅) → (𝐺‘∪ 𝑦) = ((𝐺‘∪ 𝑦) ∪ if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅)))
136	135	eleq1d 2819	. . . . . . . . . . . . . 14 ⊢ (∅ = if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅) → ((𝐺‘∪ 𝑦) ∈ 𝐴 ↔ ((𝐺‘∪ 𝑦) ∪ if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅)) ∈ 𝐴))
137		simpr 484	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ ¬ 𝑦 = ∪ 𝑦) ∧ ((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴) → ((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴)
138		fveq2 6876	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = ∪ 𝑦 → (𝐺‘𝑎) = (𝐺‘∪ 𝑦))
139	138	eleq1d 2819	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = ∪ 𝑦 → ((𝐺‘𝑎) ∈ 𝐴 ↔ (𝐺‘∪ 𝑦) ∈ 𝐴))
140		simplrr 777	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ ¬ 𝑦 = ∪ 𝑦) → ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)
141		vuniex 7733	. . . . . . . . . . . . . . . . . 18 ⊢ ∪ 𝑦 ∈ V
142	141	sucid 6436	. . . . . . . . . . . . . . . . 17 ⊢ ∪ 𝑦 ∈ suc ∪ 𝑦
143		eloni 6362	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ On → Ord 𝑦)
144		orduniorsuc 7824	. . . . . . . . . . . . . . . . . . 19 ⊢ (Ord 𝑦 → (𝑦 = ∪ 𝑦 ∨ 𝑦 = suc ∪ 𝑦))
145	27, 143, 144	3syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) → (𝑦 = ∪ 𝑦 ∨ 𝑦 = suc ∪ 𝑦))
146	145	orcanai 1004	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ ¬ 𝑦 = ∪ 𝑦) → 𝑦 = suc ∪ 𝑦)
147	142, 146	eleqtrrid 2841	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ ¬ 𝑦 = ∪ 𝑦) → ∪ 𝑦 ∈ 𝑦)
148	139, 140, 147	rspcdva 3602	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ ¬ 𝑦 = ∪ 𝑦) → (𝐺‘∪ 𝑦) ∈ 𝐴)
149	148	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ ¬ 𝑦 = ∪ 𝑦) ∧ ¬ ((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴) → (𝐺‘∪ 𝑦) ∈ 𝐴)
150	132, 136, 137, 149	ifbothda 4539	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ ¬ 𝑦 = ∪ 𝑦) → ((𝐺‘∪ 𝑦) ∪ if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅)) ∈ 𝐴)
151	130, 150	ifclda 4536	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) → if(𝑦 = ∪ 𝑦, if(𝑦 = ∅, 𝐵, ∪ (𝐺 “ 𝑦)), ((𝐺‘∪ 𝑦) ∪ if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅))) ∈ 𝐴)
152	33, 151	eqeltrd 2834	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) → (𝐺‘𝑦) ∈ 𝐴)
153	152	expr 456	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵))) → (∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴 → (𝐺‘𝑦) ∈ 𝐴))
154	24, 153	sylbird 260	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵))) → (∀𝑎 ∈ 𝑦 (𝑎 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → (𝐺‘𝑎) ∈ 𝐴) → (𝐺‘𝑦) ∈ 𝐴))
155	154	ex 412	. . . . . . . 8 ⊢ (𝜑 → (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → (∀𝑎 ∈ 𝑦 (𝑎 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → (𝐺‘𝑎) ∈ 𝐴) → (𝐺‘𝑦) ∈ 𝐴)))
156	155	com23 86	. . . . . . 7 ⊢ (𝜑 → (∀𝑎 ∈ 𝑦 (𝑎 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → (𝐺‘𝑎) ∈ 𝐴) → (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → (𝐺‘𝑦) ∈ 𝐴)))
157	156	a2i 14	. . . . . 6 ⊢ ((𝜑 → ∀𝑎 ∈ 𝑦 (𝑎 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → (𝐺‘𝑎) ∈ 𝐴)) → (𝜑 → (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → (𝐺‘𝑦) ∈ 𝐴)))
158	16, 157	sylbi 217	. . . . 5 ⊢ (∀𝑎 ∈ 𝑦 (𝜑 → (𝑎 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → (𝐺‘𝑎) ∈ 𝐴)) → (𝜑 → (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → (𝐺‘𝑦) ∈ 𝐴)))
159	158	a1i 11	. . . 4 ⊢ (𝑦 ∈ On → (∀𝑎 ∈ 𝑦 (𝜑 → (𝑎 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → (𝐺‘𝑎) ∈ 𝐴)) → (𝜑 → (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → (𝐺‘𝑦) ∈ 𝐴))))
160	10, 15, 159	tfis3 7853	. . 3 ⊢ (𝐶 ∈ On → (𝜑 → (𝐶 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → (𝐺‘𝐶) ∈ 𝐴)))
161	160	impd 410	. 2 ⊢ (𝐶 ∈ On → ((𝜑 ∧ 𝐶 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵))) → (𝐺‘𝐶) ∈ 𝐴))
162	5, 161	mpcom 38	1 ⊢ ((𝜑 ∧ 𝐶 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵))) → (𝐺‘𝐶) ∈ 𝐴)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847  ∀wal 1538   = wceq 1540  ∃wex 1779   ∈ wcel 2108   ≠ wne 2932  ∀wral 3051  ∃wrex 3060  Vcvv 3459   ∖ cdif 3923   ∪ cun 3924   ∩ cin 3925   ⊆ wss 3926  ∅c0 4308  ifcif 4500  𝒫 cpw 4575  {csn 4601  ∪ cuni 4883  ∪ ciun 4967   ↦ cmpt 5201  dom cdm 5654  ran crn 5655   “ cima 5657  Ord word 6351  Oncon0 6352  suc csuc 6354  Fun wfun 6525   Fn wfn 6526  ⟶wf 6527  –onto→wfo 6529  –1-1-onto→wf1o 6530  ‘cfv 6531  recscrecs 8384  Fincfn 8959  cardccrd 9949

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-rep 5249  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402  ax-un 7729

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-reu 3360  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-pss 3946  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-int 4923  df-iun 4969  df-br 5120  df-opab 5182  df-mpt 5202  df-tr 5230  df-id 5548  df-eprel 5553  df-po 5561  df-so 5562  df-fr 5606  df-we 5608  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-pred 6290  df-ord 6355  df-on 6356  df-lim 6357  df-suc 6358  df-iota 6484  df-fun 6533  df-fn 6534  df-f 6535  df-f1 6536  df-fo 6537  df-f1o 6538  df-fv 6539  df-ov 7408  df-om 7862  df-2nd 7989  df-frecs 8280  df-wrecs 8311  df-recs 8385  df-1o 8480  df-en 8960  df-dom 8961  df-fin 8963  df-card 9953

This theorem is referenced by:  ttukeylem7  10529