Theorem ptcmplem3 21668

Description: Lemma for ptcmp 21672. (Contributed by Mario Carneiro, 26-Aug-2015.)

Hypotheses

Ref	Expression
ptcmp.1	⊢ 𝑆 = (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))
ptcmp.2	⊢ 𝑋 = X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛)
ptcmp.3	⊢ (𝜑 → 𝐴 ∈ 𝑉)
ptcmp.4	⊢ (𝜑 → 𝐹:𝐴⟶Comp)
ptcmp.5	⊢ (𝜑 → 𝑋 ∈ (UFL ∩ dom card))
ptcmplem2.5	⊢ (𝜑 → 𝑈 ⊆ ran 𝑆)
ptcmplem2.6	⊢ (𝜑 → 𝑋 = ∪ 𝑈)
ptcmplem2.7	⊢ (𝜑 → ¬ ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = ∪ 𝑧)
ptcmplem3.8	⊢ 𝐾 = {𝑢 ∈ (𝐹‘𝑘) ∣ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) ∈ 𝑈}

Assertion

Ref	Expression
ptcmplem3	⊢ (𝜑 → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (𝑓‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)))

Distinct variable groups:   𝑓,𝑘,𝑛,𝑢,𝑤,𝑧,𝐴   𝑓,𝐾,𝑢   𝑆,𝑘,𝑛,𝑢,𝑧   𝜑,𝑓,𝑘,𝑛,𝑢   𝑈,𝑘,𝑢,𝑧   𝑘,𝑉,𝑛,𝑢,𝑤,𝑧   𝑓,𝐹,𝑘,𝑛,𝑢,𝑤,𝑧   𝑓,𝑋,𝑘,𝑛,𝑢,𝑤,𝑧

Allowed substitution hints:   𝜑(𝑧,𝑤)   𝑆(𝑤,𝑓)   𝑈(𝑤,𝑓,𝑛)   𝐾(𝑧,𝑤,𝑘,𝑛)   𝑉(𝑓)

Proof of Theorem ptcmplem3

Dummy variables 𝑔 𝑚 𝑡 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ptcmp.3	. . . 4 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
2		rabexg 4739	. . . 4 ⊢ (𝐴 ∈ 𝑉 → {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1𝑜} ∈ V)
3	1, 2	syl 17	. . 3 ⊢ (𝜑 → {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1𝑜} ∈ V)
4		ptcmp.1	. . . . 5 ⊢ 𝑆 = (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))
5		ptcmp.2	. . . . 5 ⊢ 𝑋 = X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛)
6		ptcmp.4	. . . . 5 ⊢ (𝜑 → 𝐹:𝐴⟶Comp)
7		ptcmp.5	. . . . 5 ⊢ (𝜑 → 𝑋 ∈ (UFL ∩ dom card))
8		ptcmplem2.5	. . . . 5 ⊢ (𝜑 → 𝑈 ⊆ ran 𝑆)
9		ptcmplem2.6	. . . . 5 ⊢ (𝜑 → 𝑋 = ∪ 𝑈)
10		ptcmplem2.7	. . . . 5 ⊢ (𝜑 → ¬ ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = ∪ 𝑧)
11	4, 5, 1, 6, 7, 8, 9, 10	ptcmplem2 21667	. . . 4 ⊢ (𝜑 → ∪ 𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1𝑜}∪ (𝐹‘𝑘) ∈ dom card)
12		eldifi 3694	. . . . . . . 8 ⊢ (𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾) → 𝑦 ∈ ∪ (𝐹‘𝑘))
13	12	3ad2ant3 1077	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ V ∧ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → 𝑦 ∈ ∪ (𝐹‘𝑘))
14	13	rabssdv 3645	. . . . . 6 ⊢ (𝜑 → {𝑦 ∈ V ∣ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)} ⊆ ∪ (𝐹‘𝑘))
15	14	ralrimivw 2950	. . . . 5 ⊢ (𝜑 → ∀𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1𝑜} {𝑦 ∈ V ∣ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)} ⊆ ∪ (𝐹‘𝑘))
16		ss2iun 4472	. . . . 5 ⊢ (∀𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1𝑜} {𝑦 ∈ V ∣ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)} ⊆ ∪ (𝐹‘𝑘) → ∪ 𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1𝑜} {𝑦 ∈ V ∣ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)} ⊆ ∪ 𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1𝑜}∪ (𝐹‘𝑘))
17	15, 16	syl 17	. . . 4 ⊢ (𝜑 → ∪ 𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1𝑜} {𝑦 ∈ V ∣ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)} ⊆ ∪ 𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1𝑜}∪ (𝐹‘𝑘))
18		ssnum 8745	. . . 4 ⊢ ((∪ 𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1𝑜}∪ (𝐹‘𝑘) ∈ dom card ∧ ∪ 𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1𝑜} {𝑦 ∈ V ∣ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)} ⊆ ∪ 𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1𝑜}∪ (𝐹‘𝑘)) → ∪ 𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1𝑜} {𝑦 ∈ V ∣ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)} ∈ dom card)
19	11, 17, 18	syl2anc 691	. . 3 ⊢ (𝜑 → ∪ 𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1𝑜} {𝑦 ∈ V ∣ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)} ∈ dom card)
20		elrabi 3328	. . . . 5 ⊢ (𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1𝑜} → 𝑘 ∈ 𝐴)
21	10	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ¬ ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = ∪ 𝑧)
22		ssdif0 3896	. . . . . . . . 9 ⊢ (∪ (𝐹‘𝑘) ⊆ ∪ 𝐾 ↔ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾) = ∅)
23	6	ffvelrnda 6267	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐹‘𝑘) ∈ Comp)
24	23	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) → (𝐹‘𝑘) ∈ Comp)
25		ptcmplem3.8	. . . . . . . . . . . . . 14 ⊢ 𝐾 = {𝑢 ∈ (𝐹‘𝑘) ∣ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) ∈ 𝑈}
26		ssrab2 3650	. . . . . . . . . . . . . 14 ⊢ {𝑢 ∈ (𝐹‘𝑘) ∣ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) ∈ 𝑈} ⊆ (𝐹‘𝑘)
27	25, 26	eqsstri 3598	. . . . . . . . . . . . 13 ⊢ 𝐾 ⊆ (𝐹‘𝑘)
28	27	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) → 𝐾 ⊆ (𝐹‘𝑘))
29		simpr 476	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) → ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾)
30		uniss 4394	. . . . . . . . . . . . . 14 ⊢ (𝐾 ⊆ (𝐹‘𝑘) → ∪ 𝐾 ⊆ ∪ (𝐹‘𝑘))
31	27, 30	mp1i 13	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) → ∪ 𝐾 ⊆ ∪ (𝐹‘𝑘))
32	29, 31	eqssd 3585	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) → ∪ (𝐹‘𝑘) = ∪ 𝐾)
33		eqid 2610	. . . . . . . . . . . . 13 ⊢ ∪ (𝐹‘𝑘) = ∪ (𝐹‘𝑘)
34	33	cmpcov 21002	. . . . . . . . . . . 12 ⊢ (((𝐹‘𝑘) ∈ Comp ∧ 𝐾 ⊆ (𝐹‘𝑘) ∧ ∪ (𝐹‘𝑘) = ∪ 𝐾) → ∃𝑡 ∈ (𝒫 𝐾 ∩ Fin)∪ (𝐹‘𝑘) = ∪ 𝑡)
35	24, 28, 32, 34	syl3anc 1318	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) → ∃𝑡 ∈ (𝒫 𝐾 ∩ Fin)∪ (𝐹‘𝑘) = ∪ 𝑡)
36		elfpw 8151	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ↔ (𝑡 ⊆ 𝐾 ∧ 𝑡 ∈ Fin))
37	36	simplbi 475	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) → 𝑡 ⊆ 𝐾)
38	37	ad2antrl 760	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → 𝑡 ⊆ 𝐾)
39	38	sselda 3568	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑥 ∈ 𝑡) → 𝑥 ∈ 𝐾)
40		imaeq2 5381	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢 = 𝑥 → (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) = (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥))
41	40	eleq1d 2672	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑢 = 𝑥 → ((◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) ∈ 𝑈 ↔ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) ∈ 𝑈))
42	41, 25	elrab2 3333	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ 𝐾 ↔ (𝑥 ∈ (𝐹‘𝑘) ∧ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) ∈ 𝑈))
43	42	simprbi 479	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ 𝐾 → (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) ∈ 𝑈)
44	39, 43	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑥 ∈ 𝑡) → (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) ∈ 𝑈)
45		eqid 2610	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) = (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥))
46	44, 45	fmptd 6292	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)):𝑡⟶𝑈)
47		frn 5966	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)):𝑡⟶𝑈 → ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) ⊆ 𝑈)
48	46, 47	syl 17	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) ⊆ 𝑈)
49	36	simprbi 479	. . . . . . . . . . . . . . 15 ⊢ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) → 𝑡 ∈ Fin)
50	49	ad2antrl 760	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → 𝑡 ∈ Fin)
51	45	rnmpt 5292	. . . . . . . . . . . . . . 15 ⊢ ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) = {𝑓 ∣ ∃𝑥 ∈ 𝑡 𝑓 = (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)}
52		abrexfi 8149	. . . . . . . . . . . . . . 15 ⊢ (𝑡 ∈ Fin → {𝑓 ∣ ∃𝑥 ∈ 𝑡 𝑓 = (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)} ∈ Fin)
53	51, 52	syl5eqel 2692	. . . . . . . . . . . . . 14 ⊢ (𝑡 ∈ Fin → ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) ∈ Fin)
54	50, 53	syl 17	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) ∈ Fin)
55		elfpw 8151	. . . . . . . . . . . . 13 ⊢ (ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) ∈ (𝒫 𝑈 ∩ Fin) ↔ (ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) ⊆ 𝑈 ∧ ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) ∈ Fin))
56	48, 54, 55	sylanbrc 695	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) ∈ (𝒫 𝑈 ∩ Fin))
57		simp-4r 803	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑓 ∈ 𝑋) → 𝑘 ∈ 𝐴)
58		simpr 476	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑓 ∈ 𝑋) → 𝑓 ∈ 𝑋)
59	58, 5	syl6eleq 2698	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑓 ∈ 𝑋) → 𝑓 ∈ X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛))
60		vex 3176	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 𝑓 ∈ V
61	60	elixp 7801	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓 ∈ X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛) ↔ (𝑓 Fn 𝐴 ∧ ∀𝑛 ∈ 𝐴 (𝑓‘𝑛) ∈ ∪ (𝐹‘𝑛)))
62	61	simprbi 479	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓 ∈ X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛) → ∀𝑛 ∈ 𝐴 (𝑓‘𝑛) ∈ ∪ (𝐹‘𝑛))
63	59, 62	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑓 ∈ 𝑋) → ∀𝑛 ∈ 𝐴 (𝑓‘𝑛) ∈ ∪ (𝐹‘𝑛))
64		fveq2 6103	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = 𝑘 → (𝑓‘𝑛) = (𝑓‘𝑘))
65		fveq2 6103	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 = 𝑘 → (𝐹‘𝑛) = (𝐹‘𝑘))
66	65	unieqd 4382	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = 𝑘 → ∪ (𝐹‘𝑛) = ∪ (𝐹‘𝑘))
67	64, 66	eleq12d 2682	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = 𝑘 → ((𝑓‘𝑛) ∈ ∪ (𝐹‘𝑛) ↔ (𝑓‘𝑘) ∈ ∪ (𝐹‘𝑘)))
68	67	rspcv 3278	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 ∈ 𝐴 → (∀𝑛 ∈ 𝐴 (𝑓‘𝑛) ∈ ∪ (𝐹‘𝑛) → (𝑓‘𝑘) ∈ ∪ (𝐹‘𝑘)))
69	57, 63, 68	sylc 63	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑓 ∈ 𝑋) → (𝑓‘𝑘) ∈ ∪ (𝐹‘𝑘))
70		simplrr 797	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑓 ∈ 𝑋) → ∪ (𝐹‘𝑘) = ∪ 𝑡)
71	69, 70	eleqtrd 2690	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑓 ∈ 𝑋) → (𝑓‘𝑘) ∈ ∪ 𝑡)
72		eluni2 4376	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓‘𝑘) ∈ ∪ 𝑡 ↔ ∃𝑥 ∈ 𝑡 (𝑓‘𝑘) ∈ 𝑥)
73	71, 72	sylib 207	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑓 ∈ 𝑋) → ∃𝑥 ∈ 𝑡 (𝑓‘𝑘) ∈ 𝑥)
74		fveq1 6102	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = 𝑓 → (𝑤‘𝑘) = (𝑓‘𝑘))
75	74	eleq1d 2672	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 = 𝑓 → ((𝑤‘𝑘) ∈ 𝑥 ↔ (𝑓‘𝑘) ∈ 𝑥))
76		eqid 2610	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) = (𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘))
77	76	mptpreima 5545	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) = {𝑤 ∈ 𝑋 ∣ (𝑤‘𝑘) ∈ 𝑥}
78	75, 77	elrab2 3333	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 ∈ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) ↔ (𝑓 ∈ 𝑋 ∧ (𝑓‘𝑘) ∈ 𝑥))
79	78	baib 942	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 ∈ 𝑋 → (𝑓 ∈ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) ↔ (𝑓‘𝑘) ∈ 𝑥))
80	79	ad2antlr 759	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑓 ∈ 𝑋) ∧ 𝑥 ∈ 𝑡) → (𝑓 ∈ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) ↔ (𝑓‘𝑘) ∈ 𝑥))
81	80	rexbidva 3031	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑓 ∈ 𝑋) → (∃𝑥 ∈ 𝑡 𝑓 ∈ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) ↔ ∃𝑥 ∈ 𝑡 (𝑓‘𝑘) ∈ 𝑥))
82	73, 81	mpbird 246	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑓 ∈ 𝑋) → ∃𝑥 ∈ 𝑡 𝑓 ∈ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥))
83		eliun 4460	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 ∈ ∪ 𝑥 ∈ 𝑡 (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) ↔ ∃𝑥 ∈ 𝑡 𝑓 ∈ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥))
84	82, 83	sylibr 223	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑓 ∈ 𝑋) → 𝑓 ∈ ∪ 𝑥 ∈ 𝑡 (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥))
85	84	ex 449	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → (𝑓 ∈ 𝑋 → 𝑓 ∈ ∪ 𝑥 ∈ 𝑡 (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)))
86	85	ssrdv 3574	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → 𝑋 ⊆ ∪ 𝑥 ∈ 𝑡 (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥))
87	44	ralrimiva 2949	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → ∀𝑥 ∈ 𝑡 (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) ∈ 𝑈)
88		dfiun2g 4488	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑥 ∈ 𝑡 (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) ∈ 𝑈 → ∪ 𝑥 ∈ 𝑡 (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) = ∪ {𝑓 ∣ ∃𝑥 ∈ 𝑡 𝑓 = (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)})
89	87, 88	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → ∪ 𝑥 ∈ 𝑡 (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) = ∪ {𝑓 ∣ ∃𝑥 ∈ 𝑡 𝑓 = (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)})
90	51	unieqi 4381	. . . . . . . . . . . . . . 15 ⊢ ∪ ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) = ∪ {𝑓 ∣ ∃𝑥 ∈ 𝑡 𝑓 = (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)}
91	89, 90	syl6eqr 2662	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → ∪ 𝑥 ∈ 𝑡 (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) = ∪ ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)))
92	86, 91	sseqtrd 3604	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → 𝑋 ⊆ ∪ ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)))
93	48	unissd 4398	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → ∪ ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) ⊆ ∪ 𝑈)
94	9	ad3antrrr 762	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → 𝑋 = ∪ 𝑈)
95	93, 94	sseqtr4d 3605	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → ∪ ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) ⊆ 𝑋)
96	92, 95	eqssd 3585	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → 𝑋 = ∪ ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)))
97		unieq 4380	. . . . . . . . . . . . . 14 ⊢ (𝑧 = ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) → ∪ 𝑧 = ∪ ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)))
98	97	eqeq2d 2620	. . . . . . . . . . . . 13 ⊢ (𝑧 = ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) → (𝑋 = ∪ 𝑧 ↔ 𝑋 = ∪ ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥))))
99	98	rspcev 3282	. . . . . . . . . . . 12 ⊢ ((ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑋 = ∪ ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥))) → ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = ∪ 𝑧)
100	56, 96, 99	syl2anc 691	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = ∪ 𝑧)
101	35, 100	rexlimddv 3017	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) → ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = ∪ 𝑧)
102	101	ex 449	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (∪ (𝐹‘𝑘) ⊆ ∪ 𝐾 → ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = ∪ 𝑧))
103	22, 102	syl5bir 232	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((∪ (𝐹‘𝑘) ∖ ∪ 𝐾) = ∅ → ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = ∪ 𝑧))
104	21, 103	mtod 188	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ¬ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾) = ∅)
105		neq0 3889	. . . . . . 7 ⊢ (¬ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾) = ∅ ↔ ∃𝑦 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))
106	104, 105	sylib 207	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ∃𝑦 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))
107		rexv 3193	. . . . . 6 ⊢ (∃𝑦 ∈ V 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾) ↔ ∃𝑦 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))
108	106, 107	sylibr 223	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ∃𝑦 ∈ V 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))
109	20, 108	sylan2 490	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1𝑜}) → ∃𝑦 ∈ V 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))
110	109	ralrimiva 2949	. . 3 ⊢ (𝜑 → ∀𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1𝑜}∃𝑦 ∈ V 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))
111		eleq1 2676	. . . 4 ⊢ (𝑦 = (𝑔‘𝑘) → (𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾) ↔ (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)))
112	111	ac6num 9184	. . 3 ⊢ (({𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1𝑜} ∈ V ∧ ∪ 𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1𝑜} {𝑦 ∈ V ∣ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)} ∈ dom card ∧ ∀𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1𝑜}∃𝑦 ∈ V 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → ∃𝑔(𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1𝑜}⟶V ∧ ∀𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1𝑜} (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)))
113	3, 19, 110, 112	syl3anc 1318	. 2 ⊢ (𝜑 → ∃𝑔(𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1𝑜}⟶V ∧ ∀𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1𝑜} (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)))
114	1	adantr 480	. . . 4 ⊢ ((𝜑 ∧ (𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1𝑜}⟶V ∧ ∀𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1𝑜} (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))) → 𝐴 ∈ 𝑉)
115		mptexg 6389	. . . 4 ⊢ (𝐴 ∈ 𝑉 → (𝑚 ∈ 𝐴 ↦ if(∪ (𝐹‘𝑚) ≈ 1𝑜, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) ∈ V)
116	114, 115	syl 17	. . 3 ⊢ ((𝜑 ∧ (𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1𝑜}⟶V ∧ ∀𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1𝑜} (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))) → (𝑚 ∈ 𝐴 ↦ if(∪ (𝐹‘𝑚) ≈ 1𝑜, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) ∈ V)
117		fvex 6113	. . . . . . . 8 ⊢ (𝐹‘𝑚) ∈ V
118	117	uniex 6851	. . . . . . 7 ⊢ ∪ (𝐹‘𝑚) ∈ V
119	118	uniex 6851	. . . . . 6 ⊢ ∪ ∪ (𝐹‘𝑚) ∈ V
120		fvex 6113	. . . . . 6 ⊢ (𝑔‘𝑚) ∈ V
121	119, 120	ifex 4106	. . . . 5 ⊢ if(∪ (𝐹‘𝑚) ≈ 1𝑜, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚)) ∈ V
122	121	rgenw 2908	. . . 4 ⊢ ∀𝑚 ∈ 𝐴 if(∪ (𝐹‘𝑚) ≈ 1𝑜, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚)) ∈ V
123		eqid 2610	. . . . 5 ⊢ (𝑚 ∈ 𝐴 ↦ if(∪ (𝐹‘𝑚) ≈ 1𝑜, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) = (𝑚 ∈ 𝐴 ↦ if(∪ (𝐹‘𝑚) ≈ 1𝑜, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚)))
124	123	fnmpt 5933	. . . 4 ⊢ (∀𝑚 ∈ 𝐴 if(∪ (𝐹‘𝑚) ≈ 1𝑜, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚)) ∈ V → (𝑚 ∈ 𝐴 ↦ if(∪ (𝐹‘𝑚) ≈ 1𝑜, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) Fn 𝐴)
125	122, 124	mp1i 13	. . 3 ⊢ ((𝜑 ∧ (𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1𝑜}⟶V ∧ ∀𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1𝑜} (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))) → (𝑚 ∈ 𝐴 ↦ if(∪ (𝐹‘𝑚) ≈ 1𝑜, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) Fn 𝐴)
126	66	breq1d 4593	. . . . . . 7 ⊢ (𝑛 = 𝑘 → (∪ (𝐹‘𝑛) ≈ 1𝑜 ↔ ∪ (𝐹‘𝑘) ≈ 1𝑜))
127	126	notbid 307	. . . . . 6 ⊢ (𝑛 = 𝑘 → (¬ ∪ (𝐹‘𝑛) ≈ 1𝑜 ↔ ¬ ∪ (𝐹‘𝑘) ≈ 1𝑜))
128	127	ralrab 3335	. . . . 5 ⊢ (∀𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1𝑜} (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾) ↔ ∀𝑘 ∈ 𝐴 (¬ ∪ (𝐹‘𝑘) ≈ 1𝑜 → (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)))
129		iftrue 4042	. . . . . . . . . . 11 ⊢ (∪ (𝐹‘𝑘) ≈ 1𝑜 → if(∪ (𝐹‘𝑘) ≈ 1𝑜, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) = ∪ ∪ (𝐹‘𝑘))
130	129	ad2antll 761	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1𝑜}⟶V) ∧ (𝑘 ∈ 𝐴 ∧ ∪ (𝐹‘𝑘) ≈ 1𝑜)) → if(∪ (𝐹‘𝑘) ≈ 1𝑜, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) = ∪ ∪ (𝐹‘𝑘))
131	106	adantrr 749	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑘 ∈ 𝐴 ∧ ∪ (𝐹‘𝑘) ≈ 1𝑜)) → ∃𝑦 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))
132	12	adantl 481	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑘 ∈ 𝐴 ∧ ∪ (𝐹‘𝑘) ≈ 1𝑜)) ∧ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → 𝑦 ∈ ∪ (𝐹‘𝑘))
133		simplrr 797	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑘 ∈ 𝐴 ∧ ∪ (𝐹‘𝑘) ≈ 1𝑜)) ∧ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → ∪ (𝐹‘𝑘) ≈ 1𝑜)
134		en1b 7910	. . . . . . . . . . . . . . . 16 ⊢ (∪ (𝐹‘𝑘) ≈ 1𝑜 ↔ ∪ (𝐹‘𝑘) = {∪ ∪ (𝐹‘𝑘)})
135	133, 134	sylib 207	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑘 ∈ 𝐴 ∧ ∪ (𝐹‘𝑘) ≈ 1𝑜)) ∧ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → ∪ (𝐹‘𝑘) = {∪ ∪ (𝐹‘𝑘)})
136	132, 135	eleqtrd 2690	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑘 ∈ 𝐴 ∧ ∪ (𝐹‘𝑘) ≈ 1𝑜)) ∧ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → 𝑦 ∈ {∪ ∪ (𝐹‘𝑘)})
137		elsni 4142	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ {∪ ∪ (𝐹‘𝑘)} → 𝑦 = ∪ ∪ (𝐹‘𝑘))
138	136, 137	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑘 ∈ 𝐴 ∧ ∪ (𝐹‘𝑘) ≈ 1𝑜)) ∧ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → 𝑦 = ∪ ∪ (𝐹‘𝑘))
139		simpr 476	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑘 ∈ 𝐴 ∧ ∪ (𝐹‘𝑘) ≈ 1𝑜)) ∧ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))
140	138, 139	eqeltrrd 2689	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑘 ∈ 𝐴 ∧ ∪ (𝐹‘𝑘) ≈ 1𝑜)) ∧ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → ∪ ∪ (𝐹‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))
141	131, 140	exlimddv 1850	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑘 ∈ 𝐴 ∧ ∪ (𝐹‘𝑘) ≈ 1𝑜)) → ∪ ∪ (𝐹‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))
142	141	adantlr 747	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1𝑜}⟶V) ∧ (𝑘 ∈ 𝐴 ∧ ∪ (𝐹‘𝑘) ≈ 1𝑜)) → ∪ ∪ (𝐹‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))
143	130, 142	eqeltrd 2688	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1𝑜}⟶V) ∧ (𝑘 ∈ 𝐴 ∧ ∪ (𝐹‘𝑘) ≈ 1𝑜)) → if(∪ (𝐹‘𝑘) ≈ 1𝑜, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))
144	143	a1d 25	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1𝑜}⟶V) ∧ (𝑘 ∈ 𝐴 ∧ ∪ (𝐹‘𝑘) ≈ 1𝑜)) → ((¬ ∪ (𝐹‘𝑘) ≈ 1𝑜 → (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → if(∪ (𝐹‘𝑘) ≈ 1𝑜, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)))
145	144	expr 641	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1𝑜}⟶V) ∧ 𝑘 ∈ 𝐴) → (∪ (𝐹‘𝑘) ≈ 1𝑜 → ((¬ ∪ (𝐹‘𝑘) ≈ 1𝑜 → (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → if(∪ (𝐹‘𝑘) ≈ 1𝑜, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))))
146		pm2.27 41	. . . . . . . 8 ⊢ (¬ ∪ (𝐹‘𝑘) ≈ 1𝑜 → ((¬ ∪ (𝐹‘𝑘) ≈ 1𝑜 → (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)))
147		iffalse 4045	. . . . . . . . 9 ⊢ (¬ ∪ (𝐹‘𝑘) ≈ 1𝑜 → if(∪ (𝐹‘𝑘) ≈ 1𝑜, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) = (𝑔‘𝑘))
148	147	eleq1d 2672	. . . . . . . 8 ⊢ (¬ ∪ (𝐹‘𝑘) ≈ 1𝑜 → (if(∪ (𝐹‘𝑘) ≈ 1𝑜, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾) ↔ (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)))
149	146, 148	sylibrd 248	. . . . . . 7 ⊢ (¬ ∪ (𝐹‘𝑘) ≈ 1𝑜 → ((¬ ∪ (𝐹‘𝑘) ≈ 1𝑜 → (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → if(∪ (𝐹‘𝑘) ≈ 1𝑜, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)))
150	145, 149	pm2.61d1 170	. . . . . 6 ⊢ (((𝜑 ∧ 𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1𝑜}⟶V) ∧ 𝑘 ∈ 𝐴) → ((¬ ∪ (𝐹‘𝑘) ≈ 1𝑜 → (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → if(∪ (𝐹‘𝑘) ≈ 1𝑜, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)))
151	150	ralimdva 2945	. . . . 5 ⊢ ((𝜑 ∧ 𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1𝑜}⟶V) → (∀𝑘 ∈ 𝐴 (¬ ∪ (𝐹‘𝑘) ≈ 1𝑜 → (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → ∀𝑘 ∈ 𝐴 if(∪ (𝐹‘𝑘) ≈ 1𝑜, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)))
152	128, 151	syl5bi 231	. . . 4 ⊢ ((𝜑 ∧ 𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1𝑜}⟶V) → (∀𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1𝑜} (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾) → ∀𝑘 ∈ 𝐴 if(∪ (𝐹‘𝑘) ≈ 1𝑜, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)))
153	152	impr 647	. . 3 ⊢ ((𝜑 ∧ (𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1𝑜}⟶V ∧ ∀𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1𝑜} (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))) → ∀𝑘 ∈ 𝐴 if(∪ (𝐹‘𝑘) ≈ 1𝑜, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))
154		fneq1 5893	. . . . . 6 ⊢ (𝑓 = (𝑚 ∈ 𝐴 ↦ if(∪ (𝐹‘𝑚) ≈ 1𝑜, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) → (𝑓 Fn 𝐴 ↔ (𝑚 ∈ 𝐴 ↦ if(∪ (𝐹‘𝑚) ≈ 1𝑜, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) Fn 𝐴))
155		fveq1 6102	. . . . . . . . 9 ⊢ (𝑓 = (𝑚 ∈ 𝐴 ↦ if(∪ (𝐹‘𝑚) ≈ 1𝑜, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) → (𝑓‘𝑘) = ((𝑚 ∈ 𝐴 ↦ if(∪ (𝐹‘𝑚) ≈ 1𝑜, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚)))‘𝑘))
156		fveq2 6103	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑘 → (𝐹‘𝑚) = (𝐹‘𝑘))
157	156	unieqd 4382	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑘 → ∪ (𝐹‘𝑚) = ∪ (𝐹‘𝑘))
158	157	breq1d 4593	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑘 → (∪ (𝐹‘𝑚) ≈ 1𝑜 ↔ ∪ (𝐹‘𝑘) ≈ 1𝑜))
159	157	unieqd 4382	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑘 → ∪ ∪ (𝐹‘𝑚) = ∪ ∪ (𝐹‘𝑘))
160		fveq2 6103	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑘 → (𝑔‘𝑚) = (𝑔‘𝑘))
161	158, 159, 160	ifbieq12d 4063	. . . . . . . . . 10 ⊢ (𝑚 = 𝑘 → if(∪ (𝐹‘𝑚) ≈ 1𝑜, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚)) = if(∪ (𝐹‘𝑘) ≈ 1𝑜, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)))
162		fvex 6113	. . . . . . . . . . . . 13 ⊢ (𝐹‘𝑘) ∈ V
163	162	uniex 6851	. . . . . . . . . . . 12 ⊢ ∪ (𝐹‘𝑘) ∈ V
164	163	uniex 6851	. . . . . . . . . . 11 ⊢ ∪ ∪ (𝐹‘𝑘) ∈ V
165		fvex 6113	. . . . . . . . . . 11 ⊢ (𝑔‘𝑘) ∈ V
166	164, 165	ifex 4106	. . . . . . . . . 10 ⊢ if(∪ (𝐹‘𝑘) ≈ 1𝑜, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ V
167	161, 123, 166	fvmpt 6191	. . . . . . . . 9 ⊢ (𝑘 ∈ 𝐴 → ((𝑚 ∈ 𝐴 ↦ if(∪ (𝐹‘𝑚) ≈ 1𝑜, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚)))‘𝑘) = if(∪ (𝐹‘𝑘) ≈ 1𝑜, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)))
168	155, 167	sylan9eq 2664	. . . . . . . 8 ⊢ ((𝑓 = (𝑚 ∈ 𝐴 ↦ if(∪ (𝐹‘𝑚) ≈ 1𝑜, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) ∧ 𝑘 ∈ 𝐴) → (𝑓‘𝑘) = if(∪ (𝐹‘𝑘) ≈ 1𝑜, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)))
169	168	eleq1d 2672	. . . . . . 7 ⊢ ((𝑓 = (𝑚 ∈ 𝐴 ↦ if(∪ (𝐹‘𝑚) ≈ 1𝑜, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) ∧ 𝑘 ∈ 𝐴) → ((𝑓‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾) ↔ if(∪ (𝐹‘𝑘) ≈ 1𝑜, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)))
170	169	ralbidva 2968	. . . . . 6 ⊢ (𝑓 = (𝑚 ∈ 𝐴 ↦ if(∪ (𝐹‘𝑚) ≈ 1𝑜, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) → (∀𝑘 ∈ 𝐴 (𝑓‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾) ↔ ∀𝑘 ∈ 𝐴 if(∪ (𝐹‘𝑘) ≈ 1𝑜, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)))
171	154, 170	anbi12d 743	. . . . 5 ⊢ (𝑓 = (𝑚 ∈ 𝐴 ↦ if(∪ (𝐹‘𝑚) ≈ 1𝑜, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) → ((𝑓 Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (𝑓‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) ↔ ((𝑚 ∈ 𝐴 ↦ if(∪ (𝐹‘𝑚) ≈ 1𝑜, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 if(∪ (𝐹‘𝑘) ≈ 1𝑜, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))))
172	171	spcegv 3267	. . . 4 ⊢ ((𝑚 ∈ 𝐴 ↦ if(∪ (𝐹‘𝑚) ≈ 1𝑜, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) ∈ V → (((𝑚 ∈ 𝐴 ↦ if(∪ (𝐹‘𝑚) ≈ 1𝑜, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 if(∪ (𝐹‘𝑘) ≈ 1𝑜, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (𝑓‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))))
173	172	3impib 1254	. . 3 ⊢ (((𝑚 ∈ 𝐴 ↦ if(∪ (𝐹‘𝑚) ≈ 1𝑜, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) ∈ V ∧ (𝑚 ∈ 𝐴 ↦ if(∪ (𝐹‘𝑚) ≈ 1𝑜, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 if(∪ (𝐹‘𝑘) ≈ 1𝑜, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (𝑓‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)))
174	116, 125, 153, 173	syl3anc 1318	. 2 ⊢ ((𝜑 ∧ (𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1𝑜}⟶V ∧ ∀𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1𝑜} (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))) → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (𝑓‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)))
175	113, 174	exlimddv 1850	1 ⊢ (𝜑 → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (𝑓‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475  ∃wex 1695   ∈ wcel 1977  {cab 2596  ∀wral 2896  ∃wrex 2897  {crab 2900  Vcvv 3173   ∖ cdif 3537   ∩ cin 3539   ⊆ wss 3540  ∅c0 3874  ifcif 4036  𝒫 cpw 4108  {csn 4125  ∪ cuni 4372  ∪ ciun 4455   class class class wbr 4583   ↦ cmpt 4643  ^◡ccnv 5037  dom cdm 5038  ran crn 5039   “ cima 5041   Fn wfn 5799  ⟶wf 5800  ‘cfv 5804   ↦ cmpt2 6551  1_𝑜c1o 7440  Xcixp 7794   ≈ cen 7838  Fincfn 7841  cardccrd 8644  Compccmp 20999  UFLcufl 21514

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-se 4998  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-isom 5813  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-oadd 7451  df-omul 7452  df-er 7629  df-map 7746  df-ixp 7795  df-en 7842  df-dom 7843  df-fin 7845  df-wdom 8347  df-card 8648  df-acn 8651  df-cmp 21000

This theorem is referenced by:  ptcmplem4  21669