Theorem ttukeylem6 10412

Description: Lemma for ttukey 10416. (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 9844	. . . . 5 ⊢ (card‘(∪ 𝐴 ∖ 𝐵)) ∈ On
2	1	onsuci 7775	. . . 4 ⊢ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∈ On
3	2	a1i 11	. . 3 ⊢ (𝜑 → suc (card‘(∪ 𝐴 ∖ 𝐵)) ∈ On)
4		onelon 6336	. . 3 ⊢ ((suc (card‘(∪ 𝐴 ∖ 𝐵)) ∈ On ∧ 𝐶 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵))) → 𝐶 ∈ On)
5	3, 4	sylan 580	. 2 ⊢ ((𝜑 ∧ 𝐶 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵))) → 𝐶 ∈ On)
6		eleq1 2821	. . . . . 6 ⊢ (𝑦 = 𝑎 → (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ↔ 𝑎 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵))))
7		fveq2 6828	. . . . . . 7 ⊢ (𝑦 = 𝑎 → (𝐺‘𝑦) = (𝐺‘𝑎))
8	7	eleq1d 2818	. . . . . 6 ⊢ (𝑦 = 𝑎 → ((𝐺‘𝑦) ∈ 𝐴 ↔ (𝐺‘𝑎) ∈ 𝐴))
9	6, 8	imbi12d 344	. . . . 5 ⊢ (𝑦 = 𝑎 → ((𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → (𝐺‘𝑦) ∈ 𝐴) ↔ (𝑎 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → (𝐺‘𝑎) ∈ 𝐴)))
10	9	imbi2d 340	. . . 4 ⊢ (𝑦 = 𝑎 → ((𝜑 → (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → (𝐺‘𝑦) ∈ 𝐴)) ↔ (𝜑 → (𝑎 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → (𝐺‘𝑎) ∈ 𝐴))))
11		eleq1 2821	. . . . . 6 ⊢ (𝑦 = 𝐶 → (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ↔ 𝐶 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵))))
12		fveq2 6828	. . . . . . 7 ⊢ (𝑦 = 𝐶 → (𝐺‘𝑦) = (𝐺‘𝐶))
13	12	eleq1d 2818	. . . . . 6 ⊢ (𝑦 = 𝐶 → ((𝐺‘𝑦) ∈ 𝐴 ↔ (𝐺‘𝐶) ∈ 𝐴))
14	11, 13	imbi12d 344	. . . . 5 ⊢ (𝑦 = 𝐶 → ((𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → (𝐺‘𝑦) ∈ 𝐴) ↔ (𝐶 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → (𝐺‘𝐶) ∈ 𝐴)))
15	14	imbi2d 340	. . . 4 ⊢ (𝑦 = 𝐶 → ((𝜑 → (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → (𝐺‘𝑦) ∈ 𝐴)) ↔ (𝜑 → (𝐶 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → (𝐺‘𝐶) ∈ 𝐴))))
16		r19.21v 3158	. . . . . 6 ⊢ (∀𝑎 ∈ 𝑦 (𝜑 → (𝑎 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → (𝐺‘𝑎) ∈ 𝐴)) ↔ (𝜑 → ∀𝑎 ∈ 𝑦 (𝑎 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → (𝐺‘𝑎) ∈ 𝐴)))
17	2	onordi 6424	. . . . . . . . . . . . . . 15 ⊢ Ord suc (card‘(∪ 𝐴 ∖ 𝐵))
18	17	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → Ord suc (card‘(∪ 𝐴 ∖ 𝐵)))
19		ordelss 6327	. . . . . . . . . . . . . 14 ⊢ ((Ord suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ 𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵))) → 𝑦 ⊆ suc (card‘(∪ 𝐴 ∖ 𝐵)))
20	18, 19	sylan 580	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵))) → 𝑦 ⊆ suc (card‘(∪ 𝐴 ∖ 𝐵)))
21	20	sselda 3930	. . . . . . . . . . . 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 3154	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵))) → (∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴 ↔ ∀𝑎 ∈ 𝑦 (𝑎 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) → (𝐺‘𝑎) ∈ 𝐴)))
25	2	onssi 7774	. . . . . . . . . . . . . 14 ⊢ suc (card‘(∪ 𝐴 ∖ 𝐵)) ⊆ On
26		simprl 770	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) → 𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)))
27	25, 26	sselid 3928	. . . . . . . . . . . . 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 10409	. . . . . . . . . . . . 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 4154	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) → 𝑤 ∈ Fin)
37	35	elin1d 4153	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) → 𝑤 ∈ 𝒫 ∪ (𝐺 “ 𝑦))
38	37	elpwid 4558	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) → 𝑤 ⊆ ∪ (𝐺 “ 𝑦))
39	31	tfr1 8322	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 𝐺 Fn On
40		fnfun 6586	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝐺 Fn On → Fun 𝐺)
41		funiunfv 7188	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (Fun 𝐺 → ∪ 𝑣 ∈ 𝑦 (𝐺‘𝑣) = ∪ (𝐺 “ 𝑦))
42	39, 40, 41	mp2b 10	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ∪ 𝑣 ∈ 𝑦 (𝐺‘𝑣) = ∪ (𝐺 “ 𝑦)
43	38, 42	sseqtrrdi 3972	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) → 𝑤 ⊆ ∪ 𝑣 ∈ 𝑦 (𝐺‘𝑣))
44		dfss3 3919	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 ⊆ ∪ 𝑣 ∈ 𝑦 (𝐺‘𝑣) ↔ ∀𝑢 ∈ 𝑤 𝑢 ∈ ∪ 𝑣 ∈ 𝑦 (𝐺‘𝑣))
45		eliun 4945	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑢 ∈ ∪ 𝑣 ∈ 𝑦 (𝐺‘𝑣) ↔ ∃𝑣 ∈ 𝑦 𝑢 ∈ (𝐺‘𝑣))
46	45	ralbii 3079	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∀𝑢 ∈ 𝑤 𝑢 ∈ ∪ 𝑣 ∈ 𝑦 (𝐺‘𝑣) ↔ ∀𝑢 ∈ 𝑤 ∃𝑣 ∈ 𝑦 𝑢 ∈ (𝐺‘𝑣))
47	44, 46	bitri 275	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 ⊆ ∪ 𝑣 ∈ 𝑦 (𝐺‘𝑣) ↔ ∀𝑢 ∈ 𝑤 ∃𝑣 ∈ 𝑦 𝑢 ∈ (𝐺‘𝑣))
48	43, 47	sylib 218	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) → ∀𝑢 ∈ 𝑤 ∃𝑣 ∈ 𝑦 𝑢 ∈ (𝐺‘𝑣))
49		fveq2 6828	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑣 = (𝑓‘𝑢) → (𝐺‘𝑣) = (𝐺‘(𝑓‘𝑢)))
50	49	eleq2d 2819	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 = (𝑓‘𝑢) → (𝑢 ∈ (𝐺‘𝑣) ↔ 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))
51	50	ac6sfi 9175	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑤 ∈ Fin ∧ ∀𝑢 ∈ 𝑤 ∃𝑣 ∈ 𝑦 𝑢 ∈ (𝐺‘𝑣)) → ∃𝑓(𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))
52	36, 48, 51	syl2anc 584	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) → ∃𝑓(𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))
53		eleq1 2821	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 = ∅ → (𝑤 ∈ 𝐴 ↔ ∅ ∈ 𝐴))
54		simp-4l 782	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → 𝜑)
55		fveq2 6828	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑎 = ∪ ran 𝑓 → (𝐺‘𝑎) = (𝐺‘∪ ran 𝑓))
56	55	eleq1d 2818	. . . . . . . . . . . . . . . . . . . . . . . 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 6663	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑓:𝑤⟶𝑦 → ran 𝑓 ⊆ 𝑦)
62	60, 61	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → ran 𝑓 ⊆ 𝑦)
63	27	ad3antrrr 730	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → 𝑦 ∈ On)
64		onss 7724	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑦 ∈ On → 𝑦 ⊆ On)
65	63, 64	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → 𝑦 ⊆ On)
66	62, 65	sstrd 3941	. . . . . . . . . . . . . . . . . . . . . . . . . 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 6656	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑓:𝑤⟶𝑦 → 𝑓 Fn 𝑤)
70	60, 69	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → 𝑓 Fn 𝑤)
71		dffn4 6746	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑓 Fn 𝑤 ↔ 𝑓:𝑤–onto→ran 𝑓)
72	70, 71	sylib 218	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → 𝑓:𝑤–onto→ran 𝑓)
73		fofi 9204	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑤 ∈ Fin ∧ 𝑓:𝑤–onto→ran 𝑓) → ran 𝑓 ∈ Fin)
74	68, 72, 73	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → ran 𝑓 ∈ Fin)
75		dm0rn0 5868	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (dom 𝑓 = ∅ ↔ ran 𝑓 = ∅)
76	59	fdmd 6666	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2973	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) → (ran 𝑓 ≠ ∅ ↔ 𝑤 ≠ ∅))
80	79	biimpar 477	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → ran 𝑓 ≠ ∅)
81		ordunifi 9181	. . . . . . . . . . . . . . . . . . . . . . . . . 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 3931	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → ∪ ran 𝑓 ∈ 𝑦)
84	56, 58, 83	rspcdva 3574	. . . . . . . . . . . . . . . . . . . . . . 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 7020	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤) → (𝑓‘𝑢) ∈ 𝑦)
89	88	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) ∧ (𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤)) → (𝑓‘𝑢) ∈ 𝑦)
90	87, 89	sseldd 3931	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) ∧ (𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤)) → (𝑓‘𝑢) ∈ On)
91	61	ad2antrl 728	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) ∧ (𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤)) → ran 𝑓 ⊆ 𝑦)
92	91, 87	sstrd 3941	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) ∧ (𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤)) → ran 𝑓 ⊆ On)
93		vex 3441	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ 𝑓 ∈ V
94	93	rnex 7846	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ran 𝑓 ∈ V
95	94	ssonunii 7720	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 7019	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑓 Fn 𝑤 ∧ 𝑢 ∈ 𝑤) → (𝑓‘𝑢) ∈ ran 𝑓)
100	97, 98, 99	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) ∧ (𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤)) → (𝑓‘𝑢) ∈ ran 𝑓)
101		elssuni 4889	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑓‘𝑢) ∈ ran 𝑓 → (𝑓‘𝑢) ⊆ ∪ ran 𝑓)
102	100, 101	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) ∧ (𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤)) → (𝑓‘𝑢) ⊆ ∪ ran 𝑓)
103	28, 29, 30, 31	ttukeylem5 10411	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝜑 ∧ ((𝑓‘𝑢) ∈ On ∧ ∪ ran 𝑓 ∈ On ∧ (𝑓‘𝑢) ⊆ ∪ ran 𝑓)) → (𝐺‘(𝑓‘𝑢)) ⊆ (𝐺‘∪ ran 𝑓))
104	85, 90, 96, 102, 103	syl13anc 1374	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) ∧ (𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤)) → (𝐺‘(𝑓‘𝑢)) ⊆ (𝐺‘∪ ran 𝑓))
105	104	sseld 3929	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) ∧ (𝑓:𝑤⟶𝑦 ∧ 𝑢 ∈ 𝑤)) → (𝑢 ∈ (𝐺‘(𝑓‘𝑢)) → 𝑢 ∈ (𝐺‘∪ ran 𝑓)))
106	105	anassrs 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) ∧ 𝑓:𝑤⟶𝑦) ∧ 𝑢 ∈ 𝑤) → (𝑢 ∈ (𝐺‘(𝑓‘𝑢)) → 𝑢 ∈ (𝐺‘∪ ran 𝑓)))
107	106	ralimdva 3145	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 3919	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑤 ⊆ (𝐺‘∪ ran 𝑓) ↔ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘∪ ran 𝑓))
112	110, 111	sylibr 234	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → 𝑤 ⊆ (𝐺‘∪ ran 𝑓))
113	28, 29, 30	ttukeylem2 10408	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ ((𝐺‘∪ ran 𝑓) ∈ 𝐴 ∧ 𝑤 ⊆ (𝐺‘∪ ran 𝑓))) → 𝑤 ∈ 𝐴)
114	54, 84, 112, 113	syl12anc 836	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) ∧ 𝑤 ≠ ∅) → 𝑤 ∈ 𝐴)
115		0ss 4349	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ∅ ⊆ 𝐵
116	28, 29, 30	ttukeylem2 10408	. . . . . . . . . . . . . . . . . . . . . . . . 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 3014	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ∧ (𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))))) → 𝑤 ∈ 𝐴)
121	120	expr 456	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) → ((𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))) → 𝑤 ∈ 𝐴))
122	121	exlimdv 1934	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) → (∃𝑓(𝑓:𝑤⟶𝑦 ∧ ∀𝑢 ∈ 𝑤 𝑢 ∈ (𝐺‘(𝑓‘𝑢))) → 𝑤 ∈ 𝐴))
123	52, 122	mpd 15	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) ∧ 𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin)) → 𝑤 ∈ 𝐴)
124	123	ex 412	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) → (𝑤 ∈ (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) → 𝑤 ∈ 𝐴))
125	124	ssrdv 3936	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) → (𝒫 ∪ (𝐺 “ 𝑦) ∩ Fin) ⊆ 𝐴)
126	28, 29, 30	ttukeylem1 10407	. . . . . . . . . . . . . . . . 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 4510	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ 𝑦 = ∪ 𝑦) → if(𝑦 = ∅, 𝐵, ∪ (𝐺 “ 𝑦)) ∈ 𝐴)
131		uneq2 4111	. . . . . . . . . . . . . . 15 ⊢ ({(𝐹‘∪ 𝑦)} = if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅) → ((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) = ((𝐺‘∪ 𝑦) ∪ if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅)))
132	131	eleq1d 2818	. . . . . . . . . . . . . 14 ⊢ ({(𝐹‘∪ 𝑦)} = if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅) → (((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴 ↔ ((𝐺‘∪ 𝑦) ∪ if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅)) ∈ 𝐴))
133		un0 4343	. . . . . . . . . . . . . . . 16 ⊢ ((𝐺‘∪ 𝑦) ∪ ∅) = (𝐺‘∪ 𝑦)
134		uneq2 4111	. . . . . . . . . . . . . . . 16 ⊢ (∅ = if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅) → ((𝐺‘∪ 𝑦) ∪ ∅) = ((𝐺‘∪ 𝑦) ∪ if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅)))
135	133, 134	eqtr3id 2782	. . . . . . . . . . . . . . 15 ⊢ (∅ = if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅) → (𝐺‘∪ 𝑦) = ((𝐺‘∪ 𝑦) ∪ if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅)))
136	135	eleq1d 2818	. . . . . . . . . . . . . 14 ⊢ (∅ = if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅) → ((𝐺‘∪ 𝑦) ∈ 𝐴 ↔ ((𝐺‘∪ 𝑦) ∪ if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅)) ∈ 𝐴))
137		simpr 484	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ ¬ 𝑦 = ∪ 𝑦) ∧ ((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴) → ((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴)
138		fveq2 6828	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = ∪ 𝑦 → (𝐺‘𝑎) = (𝐺‘∪ 𝑦))
139	138	eleq1d 2818	. . . . . . . . . . . . . . . 16 ⊢ (𝑎 = ∪ 𝑦 → ((𝐺‘𝑎) ∈ 𝐴 ↔ (𝐺‘∪ 𝑦) ∈ 𝐴))
140		simplrr 777	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ ¬ 𝑦 = ∪ 𝑦) → ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)
141		vuniex 7678	. . . . . . . . . . . . . . . . . 18 ⊢ ∪ 𝑦 ∈ V
142	141	sucid 6395	. . . . . . . . . . . . . . . . 17 ⊢ ∪ 𝑦 ∈ suc ∪ 𝑦
143		eloni 6321	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ On → Ord 𝑦)
144		orduniorsuc 7766	. . . . . . . . . . . . . . . . . . 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 2840	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ ¬ 𝑦 = ∪ 𝑦) → ∪ 𝑦 ∈ 𝑦)
148	139, 140, 147	rspcdva 3574	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ ¬ 𝑦 = ∪ 𝑦) → (𝐺‘∪ 𝑦) ∈ 𝐴)
149	148	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ ¬ 𝑦 = ∪ 𝑦) ∧ ¬ ((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴) → (𝐺‘∪ 𝑦) ∈ 𝐴)
150	132, 136, 137, 149	ifbothda 4513	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) ∧ ¬ 𝑦 = ∪ 𝑦) → ((𝐺‘∪ 𝑦) ∪ if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅)) ∈ 𝐴)
151	130, 150	ifclda 4510	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ suc (card‘(∪ 𝐴 ∖ 𝐵)) ∧ ∀𝑎 ∈ 𝑦 (𝐺‘𝑎) ∈ 𝐴)) → if(𝑦 = ∪ 𝑦, if(𝑦 = ∅, 𝐵, ∪ (𝐺 “ 𝑦)), ((𝐺‘∪ 𝑦) ∪ if(((𝐺‘∪ 𝑦) ∪ {(𝐹‘∪ 𝑦)}) ∈ 𝐴, {(𝐹‘∪ 𝑦)}, ∅))) ∈ 𝐴)
152	33, 151	eqeltrd 2833	. . . . . . . . . . 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 7794	. . 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 1539   = wceq 1541  ∃wex 1780   ∈ wcel 2113   ≠ wne 2929  ∀wral 3048  ∃wrex 3057  Vcvv 3437   ∖ cdif 3895   ∪ cun 3896   ∩ cin 3897   ⊆ wss 3898  ∅c0 4282  ifcif 4474  𝒫 cpw 4549  {csn 4575  ∪ cuni 4858  ∪ ciun 4941   ↦ cmpt 5174  dom cdm 5619  ran crn 5620   “ cima 5622  Ord word 6310  Oncon0 6311  suc csuc 6313  Fun wfun 6480   Fn wfn 6481  ⟶wf 6482  –onto→wfo 6484  –1-1-onto→wf1o 6485  ‘cfv 6486  recscrecs 8296  Fincfn 8875  cardccrd 9835

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-rep 5219  ax-sep 5236  ax-nul 5246  ax-pow 5305  ax-pr 5372  ax-un 7674

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-ral 3049  df-rex 3058  df-reu 3348  df-rab 3397  df-v 3439  df-sbc 3738  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3918  df-nul 4283  df-if 4475  df-pw 4551  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-int 4898  df-iun 4943  df-br 5094  df-opab 5156  df-mpt 5175  df-tr 5201  df-id 5514  df-eprel 5519  df-po 5527  df-so 5528  df-fr 5572  df-we 5574  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-pred 6253  df-ord 6314  df-on 6315  df-lim 6316  df-suc 6317  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494  df-ov 7355  df-om 7803  df-2nd 7928  df-frecs 8217  df-wrecs 8248  df-recs 8297  df-1o 8391  df-en 8876  df-dom 8877  df-fin 8879  df-card 9839

This theorem is referenced by:  ttukeylem7  10413