Theorem ttukeylem6 10499

Description: Lemma for ttukey 10503. (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 9931	. . . . 5 ⊢ (card‘(∪ 𝐴 ∖ 𝐵)) ∈ On
2	1	onsuci 7836	. . . 4 ⊢ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∈ On
3	2	a1i 11	. . 3 ⊢ (𝜑 → suc (card‘(∪ 𝐴 ∖ 𝐵)) ∈ On)
4		onelon 6387	. . 3 ⊢ ((suc (card‘(∪ 𝐴 ∖ 𝐵)) ∈ On ∧ 𝐶 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵))) → 𝐶 ∈ On)
5	3, 4	sylan 591	. 2 ⊢ ((𝜑 ∧ 𝐶 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵))) → 𝐶 ∈ On)
6		eleq1 2851	. . . . . 6 ⊢ (𝑦 = 𝑎 → (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ↔ 𝑎 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵))))
7		fveq2 6883	. . . . . . 7 ⊢ (𝑦 = 𝑎 → (𝐺‘𝑦) = (𝐺‘𝑎))
8	7	eleq1d 2848	. . . . . 6 ⊢ (𝑦 = 𝑎 → ((𝐺‘𝑦) ∈ 𝐴 ↔ (𝐺‘𝑎) ∈ 𝐴))
9	6, 8	imbi12d 347	. . . . 5 ⊢ (𝑦 = 𝑎 → ((𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → (𝐺‘𝑦) ∈ 𝐴) ↔ (𝑎 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → (𝐺‘𝑎) ∈ 𝐴)))
10	9	imbi2d 343	. . . 4 ⊢ (𝑦 = 𝑎 → ((𝜑 → (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → (𝐺‘𝑦) ∈ 𝐴)) ↔ (𝜑 → (𝑎 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → (𝐺‘𝑎) ∈ 𝐴))))
11		eleq1 2851	. . . . . 6 ⊢ (𝑦 = 𝐶 → (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ↔ 𝐶 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵))))
12		fveq2 6883	. . . . . . 7 ⊢ (𝑦 = 𝐶 → (𝐺‘𝑦) = (𝐺‘𝐶))
13	12	eleq1d 2848	. . . . . 6 ⊢ (𝑦 = 𝐶 → ((𝐺‘𝑦) ∈ 𝐴 ↔ (𝐺‘𝐶) ∈ 𝐴))
14	11, 13	imbi12d 347	. . . . 5 ⊢ (𝑦 = 𝐶 → ((𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → (𝐺‘𝑦) ∈ 𝐴) ↔ (𝐶 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → (𝐺‘𝐶) ∈ 𝐴)))
15	14	imbi2d 343	. . . 4 ⊢ (𝑦 = 𝐶 → ((𝜑 → (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → (𝐺‘𝑦) ∈ 𝐴)) ↔ (𝜑 → (𝐶 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → (𝐺‘𝐶) ∈ 𝐴))))
16		r19.21v 3190	. . . . . 6 ⊢ (∀𝑎 ∈ 𝑦 (𝜑 → (𝑎 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → (𝐺‘𝑎) ∈ 𝐴)) ↔ (𝜑 → ∀𝑎 ∈ 𝑦 (𝑎 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → (𝐺‘𝑎) ∈ 𝐴)))
17	2	onordi 6476	. . . . . . . . . . . . . . 15 ⊢ Ord suc (card‘(∪ 𝐴 ∖ 𝐵))
18	17	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → Ord suc (card‘(∪ 𝐴 ∖ 𝐵)))
19		ordelss 6378	. . . . . . . . . . . . . 14 ⊢ ((Ord suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ 𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵))) → 𝑦 ⊆ suc (card‘(∪ 𝐴 ∖ 𝐵)))
20	18, 19	sylan 591	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵))) → 𝑦 ⊆ suc (card‘(∪ 𝐴 ∖ 𝐵)))
21	20	sselda 3938	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵))) ∧ 𝑎 ∈ 𝑦) → 𝑎 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)))
22		biimt 363	. . . . . . . . . . . 12 ⊢ (𝑎 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → ((𝐺‘𝑎) ∈ 𝐴 ↔ (𝑎 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → (𝐺‘𝑎) ∈ 𝐴)))
23	21, 22	syl 18	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵))) ∧ 𝑎 ∈ 𝑦) → ((𝐺‘𝑎) ∈ 𝐴 ↔ (𝑎 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → (𝐺‘𝑎) ∈ 𝐴)))
24	23	ralbidva 3186	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵))) → (∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴 ↔ ∀𝑎 ∈ 𝑦 (𝑎 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → (𝐺‘𝑎) ∈ 𝐴)))
25	2	onssi 7835	. . . . . . . . . . . . . 14 ⊢ suc (card‘(∪ 𝐴 ∖ 𝐵)) ⊆ On
26		simprl 782	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) → 𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)))
27	25, 26	sselid 3936	. . . . . . . . . . . . 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 10496	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ On) → (𝐺‘𝑦) = if(𝑦 = ∪ 𝑦, if(𝑦 = ∅, 𝐵, ∪ (𝐺 “ 𝑦)), ((𝐺‘∪ 𝑦) ∪ if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅))))
33	27, 32	syldan 602	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) → (𝐺‘𝑦) = if(𝑦 = ∪ 𝑦, if(𝑦 = ∅, 𝐵, ∪ (𝐺 “ 𝑦)), ((𝐺‘∪ 𝑦) ∪ if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅))))
34	29	ad3antrrr 742	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑦 = ∅) → 𝐵 ∈ 𝐴)
35		simpr 489	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) → 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin))
36	35	elin2d 4159	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) → 𝑤 ∈ Fin)
37	35	elin1d 4158	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) → 𝑤 ∈ 𝒫 ∪ (𝐺 “ 𝑦))
38	37	elpwid 4572	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) → 𝑤 ⊆ ∪ (𝐺 “ 𝑦))
39	31	tfr1 8385	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝐺 Fn On
40		fnfun 6637	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐺 Fn On → Fun 𝐺)
41		funiunfv 7248	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (Fun 𝐺 → ∪ 𝑣 ∈ 𝑦 (𝐺‘𝑣) = ∪ (𝐺 “ 𝑦))
42	39, 40, 41	mp2b 10	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ∪ 𝑣 ∈ 𝑦 (𝐺‘𝑣) = ∪ (𝐺 “ 𝑦)
43	38, 42	sseqtrrdi 3979	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) → 𝑤 ⊆ ∪ 𝑣 ∈ 𝑦 (𝐺‘𝑣))
44		dfss3 3927	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 ⊆ ∪ 𝑣 ∈ 𝑦 (𝐺‘𝑣) ↔ ∀𝑢 ∈ 𝑤 𝑢 ∈ ∪ 𝑣 ∈ 𝑦 (𝐺‘𝑣))
45		eliun 4961	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑢 ∈ ∪ 𝑣 ∈ 𝑦 (𝐺‘𝑣) ↔ ∃𝑣 ∈ 𝑦 𝑢 ∈ (𝐺‘𝑣))
46	45	ralbii 3111	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∀𝑢 ∈ 𝑤 𝑢 ∈ ∪ 𝑣 ∈ 𝑦 (𝐺‘𝑣) ↔ ∀𝑢 ∈ 𝑤 ∃𝑣 ∈ 𝑦 𝑢 ∈ (𝐺‘𝑣))
47	44, 46	bitri 278	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 ⊆ ∪ 𝑣 ∈ 𝑦 (𝐺‘𝑣) ↔ ∀𝑢 ∈ 𝑤 ∃𝑣 ∈ 𝑦 𝑢 ∈ (𝐺‘𝑣))
48	43, 47	sylib 221	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) → ∀𝑢 ∈ 𝑤 ∃𝑣 ∈ 𝑦 𝑢 ∈ (𝐺‘𝑣))
49		fveq2 6883	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑣 = (𝑓‘𝑢) → (𝐺‘𝑣) = (𝐺‘(𝑓‘𝑢)))
50	49	eleq2d 2849	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 = (𝑓‘𝑢) → (𝑢 ∈ (𝐺‘𝑣) ↔ 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))
51	50	ac6sfi 9245	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑤 ∈ Fin ∧ ∀𝑢 ∈ 𝑤 ∃𝑣 ∈ 𝑦 𝑢 ∈ (𝐺‘𝑣)) → ∃𝑓(𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))
52	36, 48, 51	syl2anc 595	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) → ∃𝑓(𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))
53		eleq1 2851	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 = ∅ → (𝑤 ∈ 𝐴 ↔ ∅ ∈ 𝐴))
54		simp-4l 794	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → 𝜑)
55		fveq2 6883	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑎 = ∪ ran 𝑓 → (𝐺‘𝑎) = (𝐺‘∪ ran 𝑓))
56	55	eleq1d 2848	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑎 = ∪ ran 𝑓 → ((𝐺‘𝑎) ∈ 𝐴 ↔ (𝐺‘∪ ran 𝑓) ∈ 𝐴))
57		simplrr 789	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) → ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)
58	57	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)
59		simprrl 792	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) → 𝑓:𝑤⟶𝑦)
60	59	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → 𝑓:𝑤⟶𝑦)
61		frn 6715	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑓:𝑤⟶𝑦 → ran 𝑓 ⊆ 𝑦)
62	60, 61	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → ran 𝑓 ⊆ 𝑦)
63	27	ad3antrrr 742	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → 𝑦 ∈ On)
64		onss 7785	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑦 ∈ On → 𝑦 ⊆ On)
65	63, 64	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → 𝑦 ⊆ On)
66	62, 65	sstrd 3948	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → ran 𝑓 ⊆ On)
67	36	adantrr 729	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) → 𝑤 ∈ Fin)
68	67	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → 𝑤 ∈ Fin)
69		ffn 6707	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑓:𝑤⟶𝑦 → 𝑓 Fn 𝑤)
70	60, 69	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → 𝑓 Fn 𝑤)
71		dffn4 6800	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑓 Fn 𝑤 ↔ 𝑓:𝑤–onto→ran 𝑓)
72	70, 71	sylib 221	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → 𝑓:𝑤–onto→ran 𝑓)
73		fofi 9274	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑤 ∈ Fin ∧ 𝑓:𝑤–onto→ran 𝑓) → ran 𝑓 ∈ Fin)
74	68, 72, 73	syl2anc 595	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → ran 𝑓 ∈ Fin)
75		dm0rn0 5916	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (dom 𝑓 = ∅ ↔ ran 𝑓 = ∅)
76	59	fdmd 6718	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) → dom 𝑓 = 𝑤)
77	76	eqeq1d 2765	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) → (dom 𝑓 = ∅ ↔ 𝑤 = ∅))
78	75, 77	bitr3id 288	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) → (ran 𝑓 = ∅ ↔ 𝑤 = ∅))
79	78	necon3bid 3002	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) → (ran 𝑓 ≠ ∅ ↔ 𝑤 ≠ ∅))
80	79	biimpar 482	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → ran 𝑓 ≠ ∅)
81		ordunifi 9251	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((ran 𝑓 ⊆ On ∧ ran 𝑓 ∈ Fin ∧ ran 𝑓 ≠ ∅) → ∪ ran 𝑓 ∈ ran 𝑓)
82	66, 74, 80, 81	syl3anc 1398	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → ∪ ran 𝑓 ∈ ran 𝑓)
83	62, 82	sseldd 3939	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → ∪ ran 𝑓 ∈ 𝑦)
84	56, 58, 83	rspcdva 3583	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → (𝐺‘∪ ran 𝑓) ∈ 𝐴)
85		simp-4l 794	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) ∧ (𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤)) → 𝜑)
86	27	ad3antrrr 742	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) ∧ (𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤)) → 𝑦 ∈ On)
87	86, 64	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) ∧ (𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤)) → 𝑦 ⊆ On)
88		ffvelcdm 7078	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤) → (𝑓‘𝑢) ∈ 𝑦)
89	88	adantl 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) ∧ (𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤)) → (𝑓‘𝑢) ∈ 𝑦)
90	87, 89	sseldd 3939	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) ∧ (𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤)) → (𝑓‘𝑢) ∈ On)
91	61	ad2antrl 740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) ∧ (𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤)) → ran 𝑓 ⊆ 𝑦)
92	91, 87	sstrd 3948	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) ∧ (𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤)) → ran 𝑓 ⊆ On)
93		vex 3459	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ 𝑓 ∈ V
94	93	rnex 7908	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ran 𝑓 ∈ V
95	94	ssonunii 7781	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (ran 𝑓 ⊆ On → ∪ ran 𝑓 ∈ On)
96	92, 95	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) ∧ (𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤)) → ∪ ran 𝑓 ∈ On)
97	69	ad2antrl 740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) ∧ (𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤)) → 𝑓 Fn 𝑤)
98		simprr 784	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) ∧ (𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤)) → 𝑢 ∈ 𝑤)
99		fnfvelrn 7077	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑓 Fn 𝑤 ∧ 𝑢 ∈ 𝑤) → (𝑓‘𝑢) ∈ ran 𝑓)
100	97, 98, 99	syl2anc 595	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) ∧ (𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤)) → (𝑓‘𝑢) ∈ ran 𝑓)
101		elssuni 4905	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑓‘𝑢) ∈ ran 𝑓 → (𝑓‘𝑢) ⊆ ∪ ran 𝑓)
102	100, 101	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) ∧ (𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤)) → (𝑓‘𝑢) ⊆ ∪ ran 𝑓)
103	28, 29, 30, 31	ttukeylem5 10498	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ ((𝑓‘𝑢) ∈ On ∧ ∪ ran 𝑓 ∈ On ∧ (𝑓‘𝑢) ⊆ ∪ ran 𝑓)) → (𝐺‘(𝑓‘𝑢)) ⊆ (𝐺‘∪ ran 𝑓))
104	85, 90, 96, 102, 103	syl13anc 1399	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) ∧ (𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤)) → (𝐺‘(𝑓‘𝑢)) ⊆ (𝐺‘∪ ran 𝑓))
105	104	sseld 3937	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) ∧ (𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤)) → (𝑢 ∈ (𝐺‘(𝑓‘𝑢)) → 𝑢 ∈ (𝐺‘∪ ran 𝑓)))
106	105	anassrs 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) ∧ 𝑓:𝑤⟶𝑦) ∧ 𝑢 ∈ 𝑤) → (𝑢 ∈ (𝐺‘(𝑓‘𝑢)) → 𝑢 ∈ (𝐺‘∪ ran 𝑓)))
107	106	ralimdva 3177	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) ∧ 𝑓:𝑤⟶𝑦) → (∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢)) → ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘∪ ran 𝑓)))
108	107	expimpd 458	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) → ((𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))) → ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘∪ ran 𝑓)))
109	108	impr 459	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) → ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘∪ ran 𝑓))
110	109	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘∪ ran 𝑓))
111		dfss3 3927	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑤 ⊆ (𝐺‘∪ ran 𝑓) ↔ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘∪ ran 𝑓))
112	110, 111	sylibr 237	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → 𝑤 ⊆ (𝐺‘∪ ran 𝑓))
113	28, 29, 30	ttukeylem2 10495	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ ((𝐺‘∪ ran 𝑓) ∈ 𝐴 ∧ 𝑤 ⊆ (𝐺‘∪ ran 𝑓))) → 𝑤 ∈ 𝐴)
114	54, 84, 112, 113	syl12anc 849	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → 𝑤 ∈ 𝐴)
115		0ss 4358	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ∅ ⊆ 𝐵
116	28, 29, 30	ttukeylem2 10495	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (𝐵 ∈ 𝐴 ∧ ∅ ⊆ 𝐵)) → ∅ ∈ 𝐴)
117	115, 116	mpanr2 716	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝐵 ∈ 𝐴) → ∅ ∈ 𝐴)
118	29, 117	mpdan 699	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → ∅ ∈ 𝐴)
119	118	ad3antrrr 742	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) → ∅ ∈ 𝐴)
120	53, 114, 119	pm2.61ne 3043	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) → 𝑤 ∈ 𝐴)
121	120	expr 461	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) → ((𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))) → 𝑤 ∈ 𝐴))
122	121	exlimdv 1963	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) → (∃𝑓(𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))) → 𝑤 ∈ 𝐴))
123	52, 122	mpd 16	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) → 𝑤 ∈ 𝐴)
124	123	ex 417	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) → (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) → 𝑤 ∈ 𝐴))
125	124	ssrdv 3944	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) → (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ⊆ 𝐴)
126	28, 29, 30	ttukeylem1 10494	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (∪ (𝐺 “ 𝑦) ∈ 𝐴 ↔ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ⊆ 𝐴))
127	126	ad2antrr 738	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) → (∪ (𝐺 “ 𝑦) ∈ 𝐴 ↔ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ⊆ 𝐴))
128	125, 127	mpbird 260	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) → ∪ (𝐺 “ 𝑦) ∈ 𝐴)
129	128	adantr 485	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ ¬ 𝑦 = ∅) → ∪ (𝐺 “ 𝑦) ∈ 𝐴)
130	34, 129	ifclda 4524	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) → if(𝑦 = ∅, 𝐵, ∪ (𝐺 “ 𝑦)) ∈ 𝐴)
131		uneq2 4117	. . . . . . . . . . . . . . 15 ⊢ ({(𝐹‘∪ 𝑦)} = if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅) → ((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) = ((𝐺‘∪ 𝑦) ∪ if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅)))
132	131	eleq1d 2848	. . . . . . . . . . . . . 14 ⊢ ({(𝐹‘∪ 𝑦)} = if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅) → (((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴 ↔ ((𝐺‘∪ 𝑦) ∪ if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅)) ∈ 𝐴))
133		un0 4352	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺‘∪ 𝑦) ∪ ∅) = (𝐺‘∪ 𝑦)
134		uneq2 4117	. . . . . . . . . . . . . . . 16 ⊢ (∅ = if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅) → ((𝐺‘∪ 𝑦) ∪ ∅) = ((𝐺‘∪ 𝑦) ∪ if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅)))
135	133, 134	eqtr3id 2812	. . . . . . . . . . . . . . 15 ⊢ (∅ = if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅) → (𝐺‘∪ 𝑦) = ((𝐺‘∪ 𝑦) ∪ if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅)))
136	135	eleq1d 2848	. . . . . . . . . . . . . 14 ⊢ (∅ = if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅) → ((𝐺‘∪ 𝑦) ∈ 𝐴 ↔ ((𝐺‘∪ 𝑦) ∪ if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅)) ∈ 𝐴))
137		simpr 489	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ ¬ 𝑦 = ∪ 𝑦) ∧ ((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴) → ((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴)
138		fveq2 6883	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = ∪ 𝑦 → (𝐺‘𝑎) = (𝐺‘∪ 𝑦))
139	138	eleq1d 2848	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = ∪ 𝑦 → ((𝐺‘𝑎) ∈ 𝐴 ↔ (𝐺‘∪ 𝑦) ∈ 𝐴))
140		simplrr 789	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ ¬ 𝑦 = ∪ 𝑦) → ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)
141		vuniex 7739	. . . . . . . . . . . . . . . . . 18 ⊢ ∪ 𝑦 ∈ V
142	141	sucid 6447	. . . . . . . . . . . . . . . . 17 ⊢ ∪ 𝑦 ∈ suc ∪ 𝑦
143		eloni 6372	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ On → Ord 𝑦)
144		orduniorsuc 7827	. . . . . . . . . . . . . . . . . . 19 ⊢ (Ord 𝑦 → (𝑦 = ∪ 𝑦 ∨ 𝑦 = suc ∪ 𝑦))
145	27, 143, 144	3syl 19	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) → (𝑦 = ∪ 𝑦 ∨ 𝑦 = suc ∪ 𝑦))
146	145	orcanai 1018	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ ¬ 𝑦 = ∪ 𝑦) → 𝑦 = suc ∪ 𝑦)
147	142, 146	eleqtrrid 2870	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ ¬ 𝑦 = ∪ 𝑦) → ∪ 𝑦 ∈ 𝑦)
148	139, 140, 147	rspcdva 3583	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ ¬ 𝑦 = ∪ 𝑦) → (𝐺‘∪ 𝑦) ∈ 𝐴)
149	148	adantr 485	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ ¬ 𝑦 = ∪ 𝑦) ∧ ¬ ((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴) → (𝐺‘∪ 𝑦) ∈ 𝐴)
150	132, 136, 137, 149	ifbothda 4527	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ ¬ 𝑦 = ∪ 𝑦) → ((𝐺‘∪ 𝑦) ∪ if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅)) ∈ 𝐴)
151	130, 150	ifclda 4524	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) → if(𝑦 = ∪ 𝑦, if(𝑦 = ∅, 𝐵, ∪ (𝐺 “ 𝑦)), ((𝐺‘∪ 𝑦) ∪ if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅))) ∈ 𝐴)
152	33, 151	eqeltrd 2863	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) → (𝐺‘𝑦) ∈ 𝐴)
153	152	expr 461	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵))) → (∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴 → (𝐺‘𝑦) ∈ 𝐴))
154	24, 153	sylbird 263	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵))) → (∀𝑎 ∈ 𝑦 (𝑎 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → (𝐺‘𝑎) ∈ 𝐴) → (𝐺‘𝑦) ∈ 𝐴))
155	154	ex 417	. . . . . . . 8 ⊢ (𝜑 → (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → (∀𝑎 ∈ 𝑦 (𝑎 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → (𝐺‘𝑎) ∈ 𝐴) → (𝐺‘𝑦) ∈ 𝐴)))
156	155	com23 87	. . . . . . 7 ⊢ (𝜑 → (∀𝑎 ∈ 𝑦 (𝑎 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → (𝐺‘𝑎) ∈ 𝐴) → (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → (𝐺‘𝑦) ∈ 𝐴)))
157	156	a2i 15	. . . . . 6 ⊢ ((𝜑 → ∀𝑎 ∈ 𝑦 (𝑎 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → (𝐺‘𝑎) ∈ 𝐴)) → (𝜑 → (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → (𝐺‘𝑦) ∈ 𝐴)))
158	16, 157	sylbi 220	. . . . 5 ⊢ (∀𝑎 ∈ 𝑦 (𝜑 → (𝑎 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → (𝐺‘𝑎) ∈ 𝐴)) → (𝜑 → (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → (𝐺‘𝑦) ∈ 𝐴)))
159	158	a1i 11	. . . 4 ⊢ (𝑦 ∈ On → (∀𝑎 ∈ 𝑦 (𝜑 → (𝑎 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → (𝐺‘𝑎) ∈ 𝐴)) → (𝜑 → (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → (𝐺‘𝑦) ∈ 𝐴))))
160	10, 15, 159	tfis3 7855	. . 3 ⊢ (𝐶 ∈ On → (𝜑 → (𝐶 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → (𝐺‘𝐶) ∈ 𝐴)))
161	160	impd 415	. 2 ⊢ (𝐶 ∈ On → ((𝜑 ∧ 𝐶 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵))) → (𝐺‘𝐶) ∈ 𝐴))
162	5, 161	mpcom 39	1 ⊢ ((𝜑 ∧ 𝐶 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵))) → (𝐺‘𝐶) ∈ 𝐴)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   ∨ wo 860  ∀wal 1568   = wceq 1570  ∃wex 1809   ∈ wcel 2143   ≠ wne 2958  ∀wral 3079  ∃wrex 3089  Vcvv 3455   ∖ cdif 3903   ∪ cun 3904   ∩ cin 3905   ⊆ wss 3906  ∅c0 4287  ifcif 4488  𝒫 cpw 4563  {csn 4590  ∪ cuni 4873  ∪ ciun 4957   ↦ cmpt 5193  dom cdm 5663  ran crn 5664   “ cima 5666  Ord word 6361  Oncon0 6362  suc csuc 6364  Fun wfun 6532   Fn wfn 6533  ⟶wf 6534  –onto→wfo 6536  –1-1-onto→wf1o 6537  ‘cfv 6538  recscrecs 8358  Fincfn 8944  cardccrd 9922

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-rep 5239  ax-sep 5258  ax-nul 5270  ax-pow 5338  ax-pr 5406  ax-un 7734

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3746  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4288  df-if 4489  df-pw 4565  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-int 4914  df-iun 4959  df-br 5111  df-opab 5175  df-mpt 5194  df-tr 5220  df-id 5558  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-we 5618  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-ov 7415  df-om 7864  df-2nd 7988  df-frecs 8279  df-wrecs 8310  df-recs 8359  df-1o 8454  df-en 8945  df-dom 8946  df-fin 8948  df-card 9926

This theorem is referenced by:  ttukeylem7  10500