Theorem ttukeylem6 10279

Description: Lemma for ttukey 10283. (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 9711	. . . . 5 ⊢ (card‘(∪ 𝐴 ∖ 𝐵)) ∈ On
2	1	onsuci 7694	. . . 4 ⊢ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∈ On
3	2	a1i 11	. . 3 ⊢ (𝜑 → suc (card‘(∪ 𝐴 ∖ 𝐵)) ∈ On)
4		onelon 6295	. . 3 ⊢ ((suc (card‘(∪ 𝐴 ∖ 𝐵)) ∈ On ∧ 𝐶 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵))) → 𝐶 ∈ On)
5	3, 4	sylan 580	. 2 ⊢ ((𝜑 ∧ 𝐶 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵))) → 𝐶 ∈ On)
6		eleq1 2827	. . . . . 6 ⊢ (𝑦 = 𝑎 → (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ↔ 𝑎 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵))))
7		fveq2 6783	. . . . . . 7 ⊢ (𝑦 = 𝑎 → (𝐺‘𝑦) = (𝐺‘𝑎))
8	7	eleq1d 2824	. . . . . 6 ⊢ (𝑦 = 𝑎 → ((𝐺‘𝑦) ∈ 𝐴 ↔ (𝐺‘𝑎) ∈ 𝐴))
9	6, 8	imbi12d 345	. . . . 5 ⊢ (𝑦 = 𝑎 → ((𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → (𝐺‘𝑦) ∈ 𝐴) ↔ (𝑎 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → (𝐺‘𝑎) ∈ 𝐴)))
10	9	imbi2d 341	. . . 4 ⊢ (𝑦 = 𝑎 → ((𝜑 → (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → (𝐺‘𝑦) ∈ 𝐴)) ↔ (𝜑 → (𝑎 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → (𝐺‘𝑎) ∈ 𝐴))))
11		eleq1 2827	. . . . . 6 ⊢ (𝑦 = 𝐶 → (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ↔ 𝐶 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵))))
12		fveq2 6783	. . . . . . 7 ⊢ (𝑦 = 𝐶 → (𝐺‘𝑦) = (𝐺‘𝐶))
13	12	eleq1d 2824	. . . . . 6 ⊢ (𝑦 = 𝐶 → ((𝐺‘𝑦) ∈ 𝐴 ↔ (𝐺‘𝐶) ∈ 𝐴))
14	11, 13	imbi12d 345	. . . . 5 ⊢ (𝑦 = 𝐶 → ((𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → (𝐺‘𝑦) ∈ 𝐴) ↔ (𝐶 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → (𝐺‘𝐶) ∈ 𝐴)))
15	14	imbi2d 341	. . . 4 ⊢ (𝑦 = 𝐶 → ((𝜑 → (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → (𝐺‘𝑦) ∈ 𝐴)) ↔ (𝜑 → (𝐶 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → (𝐺‘𝐶) ∈ 𝐴))))
16		r19.21v 3114	. . . . . 6 ⊢ (∀𝑎 ∈ 𝑦 (𝜑 → (𝑎 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → (𝐺‘𝑎) ∈ 𝐴)) ↔ (𝜑 → ∀𝑎 ∈ 𝑦 (𝑎 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → (𝐺‘𝑎) ∈ 𝐴)))
17	2	onordi 6375	. . . . . . . . . . . . . . 15 ⊢ Ord suc (card‘(∪ 𝐴 ∖ 𝐵))
18	17	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → Ord suc (card‘(∪ 𝐴 ∖ 𝐵)))
19		ordelss 6286	. . . . . . . . . . . . . 14 ⊢ ((Ord suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ 𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵))) → 𝑦 ⊆ suc (card‘(∪ 𝐴 ∖ 𝐵)))
20	18, 19	sylan 580	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵))) → 𝑦 ⊆ suc (card‘(∪ 𝐴 ∖ 𝐵)))
21	20	sselda 3922	. . . . . . . . . . . 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 3112	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵))) → (∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴 ↔ ∀𝑎 ∈ 𝑦 (𝑎 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → (𝐺‘𝑎) ∈ 𝐴)))
25	2	onssi 7693	. . . . . . . . . . . . . 14 ⊢ suc (card‘(∪ 𝐴 ∖ 𝐵)) ⊆ On
26		simprl 768	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) → 𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)))
27	25, 26	sselid 3920	. . . . . . . . . . . . 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 10276	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ On) → (𝐺‘𝑦) = if(𝑦 = ∪ 𝑦, if(𝑦 = ∅, 𝐵, ∪ (𝐺 “ 𝑦)), ((𝐺‘∪ 𝑦) ∪ if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅))))
33	27, 32	syldan 591	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) → (𝐺‘𝑦) = if(𝑦 = ∪ 𝑦, if(𝑦 = ∅, 𝐵, ∪ (𝐺 “ 𝑦)), ((𝐺‘∪ 𝑦) ∪ if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅))))
34	29	ad3antrrr 727	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑦 = ∅) → 𝐵 ∈ 𝐴)
35		simpr 485	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) → 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin))
36	35	elin2d 4134	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) → 𝑤 ∈ Fin)
37	35	elin1d 4133	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) → 𝑤 ∈ 𝒫 ∪ (𝐺 “ 𝑦))
38	37	elpwid 4545	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) → 𝑤 ⊆ ∪ (𝐺 “ 𝑦))
39	31	tfr1 8237	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝐺 Fn On
40		fnfun 6542	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐺 Fn On → Fun 𝐺)
41		funiunfv 7130	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (Fun 𝐺 → ∪ 𝑣 ∈ 𝑦 (𝐺‘𝑣) = ∪ (𝐺 “ 𝑦))
42	39, 40, 41	mp2b 10	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ∪ 𝑣 ∈ 𝑦 (𝐺‘𝑣) = ∪ (𝐺 “ 𝑦)
43	38, 42	sseqtrrdi 3973	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) → 𝑤 ⊆ ∪ 𝑣 ∈ 𝑦 (𝐺‘𝑣))
44		dfss3 3910	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 ⊆ ∪ 𝑣 ∈ 𝑦 (𝐺‘𝑣) ↔ ∀𝑢 ∈ 𝑤 𝑢 ∈ ∪ 𝑣 ∈ 𝑦 (𝐺‘𝑣))
45		eliun 4929	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑢 ∈ ∪ 𝑣 ∈ 𝑦 (𝐺‘𝑣) ↔ ∃𝑣 ∈ 𝑦 𝑢 ∈ (𝐺‘𝑣))
46	45	ralbii 3093	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∀𝑢 ∈ 𝑤 𝑢 ∈ ∪ 𝑣 ∈ 𝑦 (𝐺‘𝑣) ↔ ∀𝑢 ∈ 𝑤 ∃𝑣 ∈ 𝑦 𝑢 ∈ (𝐺‘𝑣))
47	44, 46	bitri 274	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 ⊆ ∪ 𝑣 ∈ 𝑦 (𝐺‘𝑣) ↔ ∀𝑢 ∈ 𝑤 ∃𝑣 ∈ 𝑦 𝑢 ∈ (𝐺‘𝑣))
48	43, 47	sylib 217	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) → ∀𝑢 ∈ 𝑤 ∃𝑣 ∈ 𝑦 𝑢 ∈ (𝐺‘𝑣))
49		fveq2 6783	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑣 = (𝑓‘𝑢) → (𝐺‘𝑣) = (𝐺‘(𝑓‘𝑢)))
50	49	eleq2d 2825	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 = (𝑓‘𝑢) → (𝑢 ∈ (𝐺‘𝑣) ↔ 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))
51	50	ac6sfi 9067	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑤 ∈ Fin ∧ ∀𝑢 ∈ 𝑤 ∃𝑣 ∈ 𝑦 𝑢 ∈ (𝐺‘𝑣)) → ∃𝑓(𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))
52	36, 48, 51	syl2anc 584	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) → ∃𝑓(𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))
53		eleq1 2827	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 = ∅ → (𝑤 ∈ 𝐴 ↔ ∅ ∈ 𝐴))
54		simp-4l 780	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → 𝜑)
55		fveq2 6783	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑎 = ∪ ran 𝑓 → (𝐺‘𝑎) = (𝐺‘∪ ran 𝑓))
56	55	eleq1d 2824	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑎 = ∪ ran 𝑓 → ((𝐺‘𝑎) ∈ 𝐴 ↔ (𝐺‘∪ ran 𝑓) ∈ 𝐴))
57		simplrr 775	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) → ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)
58	57	ad2antrr 723	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)
59		simprrl 778	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) → 𝑓:𝑤⟶𝑦)
60	59	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → 𝑓:𝑤⟶𝑦)
61		frn 6616	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑓:𝑤⟶𝑦 → ran 𝑓 ⊆ 𝑦)
62	60, 61	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → ran 𝑓 ⊆ 𝑦)
63	27	ad3antrrr 727	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → 𝑦 ∈ On)
64		onss 7643	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑦 ∈ On → 𝑦 ⊆ On)
65	63, 64	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → 𝑦 ⊆ On)
66	62, 65	sstrd 3932	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → ran 𝑓 ⊆ On)
67	36	adantrr 714	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) → 𝑤 ∈ Fin)
68	67	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → 𝑤 ∈ Fin)
69		ffn 6609	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑓:𝑤⟶𝑦 → 𝑓 Fn 𝑤)
70	60, 69	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → 𝑓 Fn 𝑤)
71		dffn4 6703	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑓 Fn 𝑤 ↔ 𝑓:𝑤–onto→ran 𝑓)
72	70, 71	sylib 217	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → 𝑓:𝑤–onto→ran 𝑓)
73		fofi 9114	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑤 ∈ Fin ∧ 𝑓:𝑤–onto→ran 𝑓) → ran 𝑓 ∈ Fin)
74	68, 72, 73	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → ran 𝑓 ∈ Fin)
75		dm0rn0 5837	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (dom 𝑓 = ∅ ↔ ran 𝑓 = ∅)
76	59	fdmd 6620	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) → dom 𝑓 = 𝑤)
77	76	eqeq1d 2741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) → (dom 𝑓 = ∅ ↔ 𝑤 = ∅))
78	75, 77	bitr3id 285	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) → (ran 𝑓 = ∅ ↔ 𝑤 = ∅))
79	78	necon3bid 2989	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) → (ran 𝑓 ≠ ∅ ↔ 𝑤 ≠ ∅))
80	79	biimpar 478	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → ran 𝑓 ≠ ∅)
81		ordunifi 9073	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((ran 𝑓 ⊆ On ∧ ran 𝑓 ∈ Fin ∧ ran 𝑓 ≠ ∅) → ∪ ran 𝑓 ∈ ran 𝑓)
82	66, 74, 80, 81	syl3anc 1370	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → ∪ ran 𝑓 ∈ ran 𝑓)
83	62, 82	sseldd 3923	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → ∪ ran 𝑓 ∈ 𝑦)
84	56, 58, 83	rspcdva 3563	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → (𝐺‘∪ ran 𝑓) ∈ 𝐴)
85		simp-4l 780	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) ∧ (𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤)) → 𝜑)
86	27	ad3antrrr 727	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) ∧ (𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤)) → 𝑦 ∈ On)
87	86, 64	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) ∧ (𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤)) → 𝑦 ⊆ On)
88		ffvelrn 6968	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤) → (𝑓‘𝑢) ∈ 𝑦)
89	88	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) ∧ (𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤)) → (𝑓‘𝑢) ∈ 𝑦)
90	87, 89	sseldd 3923	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) ∧ (𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤)) → (𝑓‘𝑢) ∈ On)
91	61	ad2antrl 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) ∧ (𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤)) → ran 𝑓 ⊆ 𝑦)
92	91, 87	sstrd 3932	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) ∧ (𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤)) → ran 𝑓 ⊆ On)
93		vex 3437	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ 𝑓 ∈ V
94	93	rnex 7768	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ran 𝑓 ∈ V
95	94	ssonunii 7640	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (ran 𝑓 ⊆ On → ∪ ran 𝑓 ∈ On)
96	92, 95	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) ∧ (𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤)) → ∪ ran 𝑓 ∈ On)
97	69	ad2antrl 725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) ∧ (𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤)) → 𝑓 Fn 𝑤)
98		simprr 770	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) ∧ (𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤)) → 𝑢 ∈ 𝑤)
99		fnfvelrn 6967	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑓 Fn 𝑤 ∧ 𝑢 ∈ 𝑤) → (𝑓‘𝑢) ∈ ran 𝑓)
100	97, 98, 99	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) ∧ (𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤)) → (𝑓‘𝑢) ∈ ran 𝑓)
101		elssuni 4872	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑓‘𝑢) ∈ ran 𝑓 → (𝑓‘𝑢) ⊆ ∪ ran 𝑓)
102	100, 101	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) ∧ (𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤)) → (𝑓‘𝑢) ⊆ ∪ ran 𝑓)
103	28, 29, 30, 31	ttukeylem5 10278	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ ((𝑓‘𝑢) ∈ On ∧ ∪ ran 𝑓 ∈ On ∧ (𝑓‘𝑢) ⊆ ∪ ran 𝑓)) → (𝐺‘(𝑓‘𝑢)) ⊆ (𝐺‘∪ ran 𝑓))
104	85, 90, 96, 102, 103	syl13anc 1371	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) ∧ (𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤)) → (𝐺‘(𝑓‘𝑢)) ⊆ (𝐺‘∪ ran 𝑓))
105	104	sseld 3921	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) ∧ (𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤)) → (𝑢 ∈ (𝐺‘(𝑓‘𝑢)) → 𝑢 ∈ (𝐺‘∪ ran 𝑓)))
106	105	anassrs 468	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) ∧ 𝑓:𝑤⟶𝑦) ∧ 𝑢 ∈ 𝑤) → (𝑢 ∈ (𝐺‘(𝑓‘𝑢)) → 𝑢 ∈ (𝐺‘∪ ran 𝑓)))
107	106	ralimdva 3109	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) ∧ 𝑓:𝑤⟶𝑦) → (∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢)) → ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘∪ ran 𝑓)))
108	107	expimpd 454	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) → ((𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))) → ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘∪ ran 𝑓)))
109	108	impr 455	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) → ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘∪ ran 𝑓))
110	109	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘∪ ran 𝑓))
111		dfss3 3910	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑤 ⊆ (𝐺‘∪ ran 𝑓) ↔ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘∪ ran 𝑓))
112	110, 111	sylibr 233	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → 𝑤 ⊆ (𝐺‘∪ ran 𝑓))
113	28, 29, 30	ttukeylem2 10275	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ ((𝐺‘∪ ran 𝑓) ∈ 𝐴 ∧ 𝑤 ⊆ (𝐺‘∪ ran 𝑓))) → 𝑤 ∈ 𝐴)
114	54, 84, 112, 113	syl12anc 834	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → 𝑤 ∈ 𝐴)
115		0ss 4331	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ∅ ⊆ 𝐵
116	28, 29, 30	ttukeylem2 10275	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝐵 ∈ 𝐴 ∧ ∅ ⊆ 𝐵)) → ∅ ∈ 𝐴)
117	115, 116	mpanr2 701	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝐵 ∈ 𝐴) → ∅ ∈ 𝐴)
118	29, 117	mpdan 684	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ∅ ∈ 𝐴)
119	118	ad3antrrr 727	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) → ∅ ∈ 𝐴)
120	53, 114, 119	pm2.61ne 3031	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) → 𝑤 ∈ 𝐴)
121	120	expr 457	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) → ((𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))) → 𝑤 ∈ 𝐴))
122	121	exlimdv 1937	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) → (∃𝑓(𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))) → 𝑤 ∈ 𝐴))
123	52, 122	mpd 15	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) → 𝑤 ∈ 𝐴)
124	123	ex 413	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) → (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) → 𝑤 ∈ 𝐴))
125	124	ssrdv 3928	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) → (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ⊆ 𝐴)
126	28, 29, 30	ttukeylem1 10274	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (∪ (𝐺 “ 𝑦) ∈ 𝐴 ↔ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ⊆ 𝐴))
127	126	ad2antrr 723	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) → (∪ (𝐺 “ 𝑦) ∈ 𝐴 ↔ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ⊆ 𝐴))
128	125, 127	mpbird 256	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) → ∪ (𝐺 “ 𝑦) ∈ 𝐴)
129	128	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ ¬ 𝑦 = ∅) → ∪ (𝐺 “ 𝑦) ∈ 𝐴)
130	34, 129	ifclda 4495	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) → if(𝑦 = ∅, 𝐵, ∪ (𝐺 “ 𝑦)) ∈ 𝐴)
131		uneq2 4092	. . . . . . . . . . . . . . 15 ⊢ ({(𝐹‘∪ 𝑦)} = if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅) → ((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) = ((𝐺‘∪ 𝑦) ∪ if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅)))
132	131	eleq1d 2824	. . . . . . . . . . . . . 14 ⊢ ({(𝐹‘∪ 𝑦)} = if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅) → (((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴 ↔ ((𝐺‘∪ 𝑦) ∪ if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅)) ∈ 𝐴))
133		un0 4325	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺‘∪ 𝑦) ∪ ∅) = (𝐺‘∪ 𝑦)
134		uneq2 4092	. . . . . . . . . . . . . . . 16 ⊢ (∅ = if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅) → ((𝐺‘∪ 𝑦) ∪ ∅) = ((𝐺‘∪ 𝑦) ∪ if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅)))
135	133, 134	eqtr3id 2793	. . . . . . . . . . . . . . 15 ⊢ (∅ = if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅) → (𝐺‘∪ 𝑦) = ((𝐺‘∪ 𝑦) ∪ if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅)))
136	135	eleq1d 2824	. . . . . . . . . . . . . 14 ⊢ (∅ = if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅) → ((𝐺‘∪ 𝑦) ∈ 𝐴 ↔ ((𝐺‘∪ 𝑦) ∪ if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅)) ∈ 𝐴))
137		simpr 485	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ ¬ 𝑦 = ∪ 𝑦) ∧ ((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴) → ((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴)
138		fveq2 6783	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = ∪ 𝑦 → (𝐺‘𝑎) = (𝐺‘∪ 𝑦))
139	138	eleq1d 2824	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = ∪ 𝑦 → ((𝐺‘𝑎) ∈ 𝐴 ↔ (𝐺‘∪ 𝑦) ∈ 𝐴))
140		simplrr 775	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ ¬ 𝑦 = ∪ 𝑦) → ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)
141		vuniex 7601	. . . . . . . . . . . . . . . . . 18 ⊢ ∪ 𝑦 ∈ V
142	141	sucid 6349	. . . . . . . . . . . . . . . . 17 ⊢ ∪ 𝑦 ∈ suc ∪ 𝑦
143		eloni 6280	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ On → Ord 𝑦)
144		orduniorsuc 7686	. . . . . . . . . . . . . . . . . . 19 ⊢ (Ord 𝑦 → (𝑦 = ∪ 𝑦 ∨ 𝑦 = suc ∪ 𝑦))
145	27, 143, 144	3syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) → (𝑦 = ∪ 𝑦 ∨ 𝑦 = suc ∪ 𝑦))
146	145	orcanai 1000	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ ¬ 𝑦 = ∪ 𝑦) → 𝑦 = suc ∪ 𝑦)
147	142, 146	eleqtrrid 2847	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ ¬ 𝑦 = ∪ 𝑦) → ∪ 𝑦 ∈ 𝑦)
148	139, 140, 147	rspcdva 3563	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ ¬ 𝑦 = ∪ 𝑦) → (𝐺‘∪ 𝑦) ∈ 𝐴)
149	148	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ ¬ 𝑦 = ∪ 𝑦) ∧ ¬ ((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴) → (𝐺‘∪ 𝑦) ∈ 𝐴)
150	132, 136, 137, 149	ifbothda 4498	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ ¬ 𝑦 = ∪ 𝑦) → ((𝐺‘∪ 𝑦) ∪ if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅)) ∈ 𝐴)
151	130, 150	ifclda 4495	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) → if(𝑦 = ∪ 𝑦, if(𝑦 = ∅, 𝐵, ∪ (𝐺 “ 𝑦)), ((𝐺‘∪ 𝑦) ∪ if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅))) ∈ 𝐴)
152	33, 151	eqeltrd 2840	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) → (𝐺‘𝑦) ∈ 𝐴)
153	152	expr 457	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵))) → (∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴 → (𝐺‘𝑦) ∈ 𝐴))
154	24, 153	sylbird 259	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵))) → (∀𝑎 ∈ 𝑦 (𝑎 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → (𝐺‘𝑎) ∈ 𝐴) → (𝐺‘𝑦) ∈ 𝐴))
155	154	ex 413	. . . . . . . 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 7713	. . 3 ⊢ (𝐶 ∈ On → (𝜑 → (𝐶 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → (𝐺‘𝐶) ∈ 𝐴)))
161	160	impd 411	. 2 ⊢ (𝐶 ∈ On → ((𝜑 ∧ 𝐶 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵))) → (𝐺‘𝐶) ∈ 𝐴))
162	5, 161	mpcom 38	1 ⊢ ((𝜑 ∧ 𝐶 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵))) → (𝐺‘𝐶) ∈ 𝐴)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   ∨ wo 844  ∀wal 1537   = wceq 1539  ∃wex 1782   ∈ wcel 2107   ≠ wne 2944  ∀wral 3065  ∃wrex 3066  Vcvv 3433   ∖ cdif 3885   ∪ cun 3886   ∩ cin 3887   ⊆ wss 3888  ∅c0 4257  ifcif 4460  𝒫 cpw 4534  {csn 4562  ∪ cuni 4840  ∪ ciun 4925   ↦ cmpt 5158  dom cdm 5590  ran crn 5591   “ cima 5593  Ord word 6269  Oncon0 6270  suc csuc 6272  Fun wfun 6431   Fn wfn 6432  ⟶wf 6433  –onto→wfo 6435  –1-1-onto→wf1o 6436  ‘cfv 6437  recscrecs 8210  Fincfn 8742  cardccrd 9702

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 2710  ax-rep 5210  ax-sep 5224  ax-nul 5231  ax-pow 5289  ax-pr 5353  ax-un 7597

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-ral 3070  df-rex 3071  df-reu 3073  df-rab 3074  df-v 3435  df-sbc 3718  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-pss 3907  df-nul 4258  df-if 4461  df-pw 4536  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-int 4881  df-iun 4927  df-br 5076  df-opab 5138  df-mpt 5159  df-tr 5193  df-id 5490  df-eprel 5496  df-po 5504  df-so 5505  df-fr 5545  df-we 5547  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-pred 6206  df-ord 6273  df-on 6274  df-lim 6275  df-suc 6276  df-iota 6395  df-fun 6439  df-fn 6440  df-f 6441  df-f1 6442  df-fo 6443  df-f1o 6444  df-fv 6445  df-ov 7287  df-om 7722  df-2nd 7841  df-frecs 8106  df-wrecs 8137  df-recs 8211  df-1o 8306  df-er 8507  df-en 8743  df-dom 8744  df-fin 8746  df-card 9706

This theorem is referenced by:  ttukeylem7  10280