Theorem ttukeylem6 10504

Description: Lemma for ttukey 10508. (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 9934	. . . . 5 ⊢ (card‘(∪ 𝐴 ∖ 𝐵)) ∈ On
2	1	onsuci 7821	. . . 4 ⊢ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∈ On
3	2	a1i 11	. . 3 ⊢ (𝜑 → suc (card‘(∪ 𝐴 ∖ 𝐵)) ∈ On)
4		onelon 6385	. . 3 ⊢ ((suc (card‘(∪ 𝐴 ∖ 𝐵)) ∈ On ∧ 𝐶 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵))) → 𝐶 ∈ On)
5	3, 4	sylan 581	. 2 ⊢ ((𝜑 ∧ 𝐶 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵))) → 𝐶 ∈ On)
6		eleq1 2822	. . . . . 6 ⊢ (𝑦 = 𝑎 → (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ↔ 𝑎 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵))))
7		fveq2 6887	. . . . . . 7 ⊢ (𝑦 = 𝑎 → (𝐺‘𝑦) = (𝐺‘𝑎))
8	7	eleq1d 2819	. . . . . 6 ⊢ (𝑦 = 𝑎 → ((𝐺‘𝑦) ∈ 𝐴 ↔ (𝐺‘𝑎) ∈ 𝐴))
9	6, 8	imbi12d 345	. . . . 5 ⊢ (𝑦 = 𝑎 → ((𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → (𝐺‘𝑦) ∈ 𝐴) ↔ (𝑎 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → (𝐺‘𝑎) ∈ 𝐴)))
10	9	imbi2d 341	. . . 4 ⊢ (𝑦 = 𝑎 → ((𝜑 → (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → (𝐺‘𝑦) ∈ 𝐴)) ↔ (𝜑 → (𝑎 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → (𝐺‘𝑎) ∈ 𝐴))))
11		eleq1 2822	. . . . . 6 ⊢ (𝑦 = 𝐶 → (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ↔ 𝐶 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵))))
12		fveq2 6887	. . . . . . 7 ⊢ (𝑦 = 𝐶 → (𝐺‘𝑦) = (𝐺‘𝐶))
13	12	eleq1d 2819	. . . . . 6 ⊢ (𝑦 = 𝐶 → ((𝐺‘𝑦) ∈ 𝐴 ↔ (𝐺‘𝐶) ∈ 𝐴))
14	11, 13	imbi12d 345	. . . . 5 ⊢ (𝑦 = 𝐶 → ((𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → (𝐺‘𝑦) ∈ 𝐴) ↔ (𝐶 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → (𝐺‘𝐶) ∈ 𝐴)))
15	14	imbi2d 341	. . . 4 ⊢ (𝑦 = 𝐶 → ((𝜑 → (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → (𝐺‘𝑦) ∈ 𝐴)) ↔ (𝜑 → (𝐶 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → (𝐺‘𝐶) ∈ 𝐴))))
16		r19.21v 3180	. . . . . 6 ⊢ (∀𝑎 ∈ 𝑦 (𝜑 → (𝑎 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → (𝐺‘𝑎) ∈ 𝐴)) ↔ (𝜑 → ∀𝑎 ∈ 𝑦 (𝑎 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → (𝐺‘𝑎) ∈ 𝐴)))
17	2	onordi 6471	. . . . . . . . . . . . . . 15 ⊢ Ord suc (card‘(∪ 𝐴 ∖ 𝐵))
18	17	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → Ord suc (card‘(∪ 𝐴 ∖ 𝐵)))
19		ordelss 6376	. . . . . . . . . . . . . 14 ⊢ ((Ord suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ 𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵))) → 𝑦 ⊆ suc (card‘(∪ 𝐴 ∖ 𝐵)))
20	18, 19	sylan 581	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵))) → 𝑦 ⊆ suc (card‘(∪ 𝐴 ∖ 𝐵)))
21	20	sselda 3980	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵))) ∧ 𝑎 ∈ 𝑦) → 𝑎 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)))
22		biimt 361	. . . . . . . . . . . 12 ⊢ (𝑎 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → ((𝐺‘𝑎) ∈ 𝐴 ↔ (𝑎 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → (𝐺‘𝑎) ∈ 𝐴)))
23	21, 22	syl 17	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵))) ∧ 𝑎 ∈ 𝑦) → ((𝐺‘𝑎) ∈ 𝐴 ↔ (𝑎 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → (𝐺‘𝑎) ∈ 𝐴)))
24	23	ralbidva 3176	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵))) → (∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴 ↔ ∀𝑎 ∈ 𝑦 (𝑎 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → (𝐺‘𝑎) ∈ 𝐴)))
25	2	onssi 7820	. . . . . . . . . . . . . 14 ⊢ suc (card‘(∪ 𝐴 ∖ 𝐵)) ⊆ On
26		simprl 770	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) → 𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)))
27	25, 26	sselid 3978	. . . . . . . . . . . . 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 10501	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ On) → (𝐺‘𝑦) = if(𝑦 = ∪ 𝑦, if(𝑦 = ∅, 𝐵, ∪ (𝐺 “ 𝑦)), ((𝐺‘∪ 𝑦) ∪ if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅))))
33	27, 32	syldan 592	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) → (𝐺‘𝑦) = if(𝑦 = ∪ 𝑦, if(𝑦 = ∅, 𝐵, ∪ (𝐺 “ 𝑦)), ((𝐺‘∪ 𝑦) ∪ if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅))))
34	29	ad3antrrr 729	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑦 = ∅) → 𝐵 ∈ 𝐴)
35		simpr 486	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) → 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin))
36	35	elin2d 4197	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) → 𝑤 ∈ Fin)
37	35	elin1d 4196	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) → 𝑤 ∈ 𝒫 ∪ (𝐺 “ 𝑦))
38	37	elpwid 4609	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) → 𝑤 ⊆ ∪ (𝐺 “ 𝑦))
39	31	tfr1 8391	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝐺 Fn On
40		fnfun 6645	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐺 Fn On → Fun 𝐺)
41		funiunfv 7241	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (Fun 𝐺 → ∪ 𝑣 ∈ 𝑦 (𝐺‘𝑣) = ∪ (𝐺 “ 𝑦))
42	39, 40, 41	mp2b 10	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ∪ 𝑣 ∈ 𝑦 (𝐺‘𝑣) = ∪ (𝐺 “ 𝑦)
43	38, 42	sseqtrrdi 4031	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) → 𝑤 ⊆ ∪ 𝑣 ∈ 𝑦 (𝐺‘𝑣))
44		dfss3 3968	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 ⊆ ∪ 𝑣 ∈ 𝑦 (𝐺‘𝑣) ↔ ∀𝑢 ∈ 𝑤 𝑢 ∈ ∪ 𝑣 ∈ 𝑦 (𝐺‘𝑣))
45		eliun 4999	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑢 ∈ ∪ 𝑣 ∈ 𝑦 (𝐺‘𝑣) ↔ ∃𝑣 ∈ 𝑦 𝑢 ∈ (𝐺‘𝑣))
46	45	ralbii 3094	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∀𝑢 ∈ 𝑤 𝑢 ∈ ∪ 𝑣 ∈ 𝑦 (𝐺‘𝑣) ↔ ∀𝑢 ∈ 𝑤 ∃𝑣 ∈ 𝑦 𝑢 ∈ (𝐺‘𝑣))
47	44, 46	bitri 275	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 ⊆ ∪ 𝑣 ∈ 𝑦 (𝐺‘𝑣) ↔ ∀𝑢 ∈ 𝑤 ∃𝑣 ∈ 𝑦 𝑢 ∈ (𝐺‘𝑣))
48	43, 47	sylib 217	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) → ∀𝑢 ∈ 𝑤 ∃𝑣 ∈ 𝑦 𝑢 ∈ (𝐺‘𝑣))
49		fveq2 6887	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑣 = (𝑓‘𝑢) → (𝐺‘𝑣) = (𝐺‘(𝑓‘𝑢)))
50	49	eleq2d 2820	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 = (𝑓‘𝑢) → (𝑢 ∈ (𝐺‘𝑣) ↔ 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))
51	50	ac6sfi 9282	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑤 ∈ Fin ∧ ∀𝑢 ∈ 𝑤 ∃𝑣 ∈ 𝑦 𝑢 ∈ (𝐺‘𝑣)) → ∃𝑓(𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))
52	36, 48, 51	syl2anc 585	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) → ∃𝑓(𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))
53		eleq1 2822	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 = ∅ → (𝑤 ∈ 𝐴 ↔ ∅ ∈ 𝐴))
54		simp-4l 782	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → 𝜑)
55		fveq2 6887	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑎 = ∪ ran 𝑓 → (𝐺‘𝑎) = (𝐺‘∪ ran 𝑓))
56	55	eleq1d 2819	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑎 = ∪ ran 𝑓 → ((𝐺‘𝑎) ∈ 𝐴 ↔ (𝐺‘∪ ran 𝑓) ∈ 𝐴))
57		simplrr 777	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) → ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)
58	57	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)
59		simprrl 780	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) → 𝑓:𝑤⟶𝑦)
60	59	adantr 482	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → 𝑓:𝑤⟶𝑦)
61		frn 6720	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑓:𝑤⟶𝑦 → ran 𝑓 ⊆ 𝑦)
62	60, 61	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → ran 𝑓 ⊆ 𝑦)
63	27	ad3antrrr 729	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → 𝑦 ∈ On)
64		onss 7766	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑦 ∈ On → 𝑦 ⊆ On)
65	63, 64	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → 𝑦 ⊆ On)
66	62, 65	sstrd 3990	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → ran 𝑓 ⊆ On)
67	36	adantrr 716	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) → 𝑤 ∈ Fin)
68	67	adantr 482	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → 𝑤 ∈ Fin)
69		ffn 6713	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑓:𝑤⟶𝑦 → 𝑓 Fn 𝑤)
70	60, 69	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → 𝑓 Fn 𝑤)
71		dffn4 6807	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑓 Fn 𝑤 ↔ 𝑓:𝑤–onto→ran 𝑓)
72	70, 71	sylib 217	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → 𝑓:𝑤–onto→ran 𝑓)
73		fofi 9333	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑤 ∈ Fin ∧ 𝑓:𝑤–onto→ran 𝑓) → ran 𝑓 ∈ Fin)
74	68, 72, 73	syl2anc 585	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → ran 𝑓 ∈ Fin)
75		dm0rn0 5921	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (dom 𝑓 = ∅ ↔ ran 𝑓 = ∅)
76	59	fdmd 6724	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) → dom 𝑓 = 𝑤)
77	76	eqeq1d 2735	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) → (dom 𝑓 = ∅ ↔ 𝑤 = ∅))
78	75, 77	bitr3id 285	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) → (ran 𝑓 = ∅ ↔ 𝑤 = ∅))
79	78	necon3bid 2986	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) → (ran 𝑓 ≠ ∅ ↔ 𝑤 ≠ ∅))
80	79	biimpar 479	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → ran 𝑓 ≠ ∅)
81		ordunifi 9288	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((ran 𝑓 ⊆ On ∧ ran 𝑓 ∈ Fin ∧ ran 𝑓 ≠ ∅) → ∪ ran 𝑓 ∈ ran 𝑓)
82	66, 74, 80, 81	syl3anc 1372	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → ∪ ran 𝑓 ∈ ran 𝑓)
83	62, 82	sseldd 3981	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → ∪ ran 𝑓 ∈ 𝑦)
84	56, 58, 83	rspcdva 3612	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → (𝐺‘∪ ran 𝑓) ∈ 𝐴)
85		simp-4l 782	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) ∧ (𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤)) → 𝜑)
86	27	ad3antrrr 729	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) ∧ (𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤)) → 𝑦 ∈ On)
87	86, 64	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) ∧ (𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤)) → 𝑦 ⊆ On)
88		ffvelcdm 7078	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤) → (𝑓‘𝑢) ∈ 𝑦)
89	88	adantl 483	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) ∧ (𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤)) → (𝑓‘𝑢) ∈ 𝑦)
90	87, 89	sseldd 3981	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) ∧ (𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤)) → (𝑓‘𝑢) ∈ On)
91	61	ad2antrl 727	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) ∧ (𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤)) → ran 𝑓 ⊆ 𝑦)
92	91, 87	sstrd 3990	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) ∧ (𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤)) → ran 𝑓 ⊆ On)
93		vex 3479	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ 𝑓 ∈ V
94	93	rnex 7897	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ran 𝑓 ∈ V
95	94	ssonunii 7762	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (ran 𝑓 ⊆ On → ∪ ran 𝑓 ∈ On)
96	92, 95	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) ∧ (𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤)) → ∪ ran 𝑓 ∈ On)
97	69	ad2antrl 727	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) ∧ (𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤)) → 𝑓 Fn 𝑤)
98		simprr 772	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) ∧ (𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤)) → 𝑢 ∈ 𝑤)
99		fnfvelrn 7077	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑓 Fn 𝑤 ∧ 𝑢 ∈ 𝑤) → (𝑓‘𝑢) ∈ ran 𝑓)
100	97, 98, 99	syl2anc 585	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) ∧ (𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤)) → (𝑓‘𝑢) ∈ ran 𝑓)
101		elssuni 4939	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑓‘𝑢) ∈ ran 𝑓 → (𝑓‘𝑢) ⊆ ∪ ran 𝑓)
102	100, 101	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) ∧ (𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤)) → (𝑓‘𝑢) ⊆ ∪ ran 𝑓)
103	28, 29, 30, 31	ttukeylem5 10503	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ ((𝑓‘𝑢) ∈ On ∧ ∪ ran 𝑓 ∈ On ∧ (𝑓‘𝑢) ⊆ ∪ ran 𝑓)) → (𝐺‘(𝑓‘𝑢)) ⊆ (𝐺‘∪ ran 𝑓))
104	85, 90, 96, 102, 103	syl13anc 1373	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) ∧ (𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤)) → (𝐺‘(𝑓‘𝑢)) ⊆ (𝐺‘∪ ran 𝑓))
105	104	sseld 3979	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) ∧ (𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤)) → (𝑢 ∈ (𝐺‘(𝑓‘𝑢)) → 𝑢 ∈ (𝐺‘∪ ran 𝑓)))
106	105	anassrs 469	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) ∧ 𝑓:𝑤⟶𝑦) ∧ 𝑢 ∈ 𝑤) → (𝑢 ∈ (𝐺‘(𝑓‘𝑢)) → 𝑢 ∈ (𝐺‘∪ ran 𝑓)))
107	106	ralimdva 3168	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) ∧ 𝑓:𝑤⟶𝑦) → (∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢)) → ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘∪ ran 𝑓)))
108	107	expimpd 455	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) → ((𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))) → ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘∪ ran 𝑓)))
109	108	impr 456	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) → ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘∪ ran 𝑓))
110	109	adantr 482	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘∪ ran 𝑓))
111		dfss3 3968	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑤 ⊆ (𝐺‘∪ ran 𝑓) ↔ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘∪ ran 𝑓))
112	110, 111	sylibr 233	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → 𝑤 ⊆ (𝐺‘∪ ran 𝑓))
113	28, 29, 30	ttukeylem2 10500	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ ((𝐺‘∪ ran 𝑓) ∈ 𝐴 ∧ 𝑤 ⊆ (𝐺‘∪ ran 𝑓))) → 𝑤 ∈ 𝐴)
114	54, 84, 112, 113	syl12anc 836	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → 𝑤 ∈ 𝐴)
115		0ss 4394	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ∅ ⊆ 𝐵
116	28, 29, 30	ttukeylem2 10500	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝐵 ∈ 𝐴 ∧ ∅ ⊆ 𝐵)) → ∅ ∈ 𝐴)
117	115, 116	mpanr2 703	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝐵 ∈ 𝐴) → ∅ ∈ 𝐴)
118	29, 117	mpdan 686	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ∅ ∈ 𝐴)
119	118	ad3antrrr 729	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) → ∅ ∈ 𝐴)
120	53, 114, 119	pm2.61ne 3028	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) → 𝑤 ∈ 𝐴)
121	120	expr 458	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) → ((𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))) → 𝑤 ∈ 𝐴))
122	121	exlimdv 1937	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) → (∃𝑓(𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))) → 𝑤 ∈ 𝐴))
123	52, 122	mpd 15	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) → 𝑤 ∈ 𝐴)
124	123	ex 414	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) → (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) → 𝑤 ∈ 𝐴))
125	124	ssrdv 3986	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) → (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ⊆ 𝐴)
126	28, 29, 30	ttukeylem1 10499	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (∪ (𝐺 “ 𝑦) ∈ 𝐴 ↔ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ⊆ 𝐴))
127	126	ad2antrr 725	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) → (∪ (𝐺 “ 𝑦) ∈ 𝐴 ↔ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ⊆ 𝐴))
128	125, 127	mpbird 257	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) → ∪ (𝐺 “ 𝑦) ∈ 𝐴)
129	128	adantr 482	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ ¬ 𝑦 = ∅) → ∪ (𝐺 “ 𝑦) ∈ 𝐴)
130	34, 129	ifclda 4561	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) → if(𝑦 = ∅, 𝐵, ∪ (𝐺 “ 𝑦)) ∈ 𝐴)
131		uneq2 4155	. . . . . . . . . . . . . . 15 ⊢ ({(𝐹‘∪ 𝑦)} = if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅) → ((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) = ((𝐺‘∪ 𝑦) ∪ if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅)))
132	131	eleq1d 2819	. . . . . . . . . . . . . 14 ⊢ ({(𝐹‘∪ 𝑦)} = if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅) → (((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴 ↔ ((𝐺‘∪ 𝑦) ∪ if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅)) ∈ 𝐴))
133		un0 4388	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺‘∪ 𝑦) ∪ ∅) = (𝐺‘∪ 𝑦)
134		uneq2 4155	. . . . . . . . . . . . . . . 16 ⊢ (∅ = if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅) → ((𝐺‘∪ 𝑦) ∪ ∅) = ((𝐺‘∪ 𝑦) ∪ if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅)))
135	133, 134	eqtr3id 2787	. . . . . . . . . . . . . . 15 ⊢ (∅ = if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅) → (𝐺‘∪ 𝑦) = ((𝐺‘∪ 𝑦) ∪ if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅)))
136	135	eleq1d 2819	. . . . . . . . . . . . . 14 ⊢ (∅ = if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅) → ((𝐺‘∪ 𝑦) ∈ 𝐴 ↔ ((𝐺‘∪ 𝑦) ∪ if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅)) ∈ 𝐴))
137		simpr 486	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ ¬ 𝑦 = ∪ 𝑦) ∧ ((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴) → ((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴)
138		fveq2 6887	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = ∪ 𝑦 → (𝐺‘𝑎) = (𝐺‘∪ 𝑦))
139	138	eleq1d 2819	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = ∪ 𝑦 → ((𝐺‘𝑎) ∈ 𝐴 ↔ (𝐺‘∪ 𝑦) ∈ 𝐴))
140		simplrr 777	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ ¬ 𝑦 = ∪ 𝑦) → ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)
141		vuniex 7723	. . . . . . . . . . . . . . . . . 18 ⊢ ∪ 𝑦 ∈ V
142	141	sucid 6442	. . . . . . . . . . . . . . . . 17 ⊢ ∪ 𝑦 ∈ suc ∪ 𝑦
143		eloni 6370	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ On → Ord 𝑦)
144		orduniorsuc 7812	. . . . . . . . . . . . . . . . . . 19 ⊢ (Ord 𝑦 → (𝑦 = ∪ 𝑦 ∨ 𝑦 = suc ∪ 𝑦))
145	27, 143, 144	3syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) → (𝑦 = ∪ 𝑦 ∨ 𝑦 = suc ∪ 𝑦))
146	145	orcanai 1002	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ ¬ 𝑦 = ∪ 𝑦) → 𝑦 = suc ∪ 𝑦)
147	142, 146	eleqtrrid 2841	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ ¬ 𝑦 = ∪ 𝑦) → ∪ 𝑦 ∈ 𝑦)
148	139, 140, 147	rspcdva 3612	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ ¬ 𝑦 = ∪ 𝑦) → (𝐺‘∪ 𝑦) ∈ 𝐴)
149	148	adantr 482	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ ¬ 𝑦 = ∪ 𝑦) ∧ ¬ ((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴) → (𝐺‘∪ 𝑦) ∈ 𝐴)
150	132, 136, 137, 149	ifbothda 4564	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ ¬ 𝑦 = ∪ 𝑦) → ((𝐺‘∪ 𝑦) ∪ if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅)) ∈ 𝐴)
151	130, 150	ifclda 4561	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) → if(𝑦 = ∪ 𝑦, if(𝑦 = ∅, 𝐵, ∪ (𝐺 “ 𝑦)), ((𝐺‘∪ 𝑦) ∪ if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅))) ∈ 𝐴)
152	33, 151	eqeltrd 2834	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) → (𝐺‘𝑦) ∈ 𝐴)
153	152	expr 458	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵))) → (∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴 → (𝐺‘𝑦) ∈ 𝐴))
154	24, 153	sylbird 260	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵))) → (∀𝑎 ∈ 𝑦 (𝑎 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → (𝐺‘𝑎) ∈ 𝐴) → (𝐺‘𝑦) ∈ 𝐴))
155	154	ex 414	. . . . . . . 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 216	. . . . 5 ⊢ (∀𝑎 ∈ 𝑦 (𝜑 → (𝑎 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → (𝐺‘𝑎) ∈ 𝐴)) → (𝜑 → (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → (𝐺‘𝑦) ∈ 𝐴)))
159	158	a1i 11	. . . 4 ⊢ (𝑦 ∈ On → (∀𝑎 ∈ 𝑦 (𝜑 → (𝑎 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → (𝐺‘𝑎) ∈ 𝐴)) → (𝜑 → (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → (𝐺‘𝑦) ∈ 𝐴))))
160	10, 15, 159	tfis3 7841	. . 3 ⊢ (𝐶 ∈ On → (𝜑 → (𝐶 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → (𝐺‘𝐶) ∈ 𝐴)))
161	160	impd 412	. 2 ⊢ (𝐶 ∈ On → ((𝜑 ∧ 𝐶 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵))) → (𝐺‘𝐶) ∈ 𝐴))
162	5, 161	mpcom 38	1 ⊢ ((𝜑 ∧ 𝐶 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵))) → (𝐺‘𝐶) ∈ 𝐴)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 397   ∨ wo 846  ∀wal 1540   = wceq 1542  ∃wex 1782   ∈ wcel 2107   ≠ wne 2941  ∀wral 3062  ∃wrex 3071  Vcvv 3475   ∖ cdif 3943   ∪ cun 3944   ∩ cin 3945   ⊆ wss 3946  ∅c0 4320  ifcif 4526  𝒫 cpw 4600  {csn 4626  ∪ cuni 4906  ∪ ciun 4995   ↦ cmpt 5229  dom cdm 5674  ran crn 5675   “ cima 5677  Ord word 6359  Oncon0 6360  suc csuc 6362  Fun wfun 6533   Fn wfn 6534  ⟶wf 6535  –onto→wfo 6537  –1-1-onto→wf1o 6538  ‘cfv 6539  recscrecs 8364  Fincfn 8934  cardccrd 9925

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5283  ax-sep 5297  ax-nul 5304  ax-pow 5361  ax-pr 5425  ax-un 7719

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3776  df-csb 3892  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-pss 3965  df-nul 4321  df-if 4527  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4907  df-int 4949  df-iun 4997  df-br 5147  df-opab 5209  df-mpt 5230  df-tr 5264  df-id 5572  df-eprel 5578  df-po 5586  df-so 5587  df-fr 5629  df-we 5631  df-xp 5680  df-rel 5681  df-cnv 5682  df-co 5683  df-dm 5684  df-rn 5685  df-res 5686  df-ima 5687  df-pred 6296  df-ord 6363  df-on 6364  df-lim 6365  df-suc 6366  df-iota 6491  df-fun 6541  df-fn 6542  df-f 6543  df-f1 6544  df-fo 6545  df-f1o 6546  df-fv 6547  df-ov 7406  df-om 7850  df-2nd 7970  df-frecs 8260  df-wrecs 8291  df-recs 8365  df-1o 8460  df-er 8698  df-en 8935  df-dom 8936  df-fin 8938  df-card 9929

This theorem is referenced by:  ttukeylem7  10505