Theorem ptcmplem3 22662

Description: Lemma for ptcmp 22666. (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 5234	. . . 4 ⊢ (𝐴 ∈ 𝑉 → {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o} ∈ V)
3	1, 2	syl 17	. . 3 ⊢ (𝜑 → {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o} ∈ 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 22661	. . . 4 ⊢ (𝜑 → ∪ 𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}∪ (𝐹‘𝑘) ∈ dom card)
12		eldifi 4103	. . . . . . . 8 ⊢ (𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾) → 𝑦 ∈ ∪ (𝐹‘𝑘))
13	12	3ad2ant3 1131	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ V ∧ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → 𝑦 ∈ ∪ (𝐹‘𝑘))
14	13	rabssdv 4051	. . . . . 6 ⊢ (𝜑 → {𝑦 ∈ V ∣ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)} ⊆ ∪ (𝐹‘𝑘))
15	14	ralrimivw 3183	. . . . 5 ⊢ (𝜑 → ∀𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o} {𝑦 ∈ V ∣ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)} ⊆ ∪ (𝐹‘𝑘))
16		ss2iun 4937	. . . . 5 ⊢ (∀𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o} {𝑦 ∈ V ∣ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)} ⊆ ∪ (𝐹‘𝑘) → ∪ 𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o} {𝑦 ∈ V ∣ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)} ⊆ ∪ 𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}∪ (𝐹‘𝑘))
17	15, 16	syl 17	. . . 4 ⊢ (𝜑 → ∪ 𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o} {𝑦 ∈ V ∣ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)} ⊆ ∪ 𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}∪ (𝐹‘𝑘))
18		ssnum 9465	. . . 4 ⊢ ((∪ 𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}∪ (𝐹‘𝑘) ∈ dom card ∧ ∪ 𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o} {𝑦 ∈ V ∣ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)} ⊆ ∪ 𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}∪ (𝐹‘𝑘)) → ∪ 𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o} {𝑦 ∈ V ∣ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)} ∈ dom card)
19	11, 17, 18	syl2anc 586	. . 3 ⊢ (𝜑 → ∪ 𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o} {𝑦 ∈ V ∣ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)} ∈ dom card)
20		elrabi 3675	. . . . 5 ⊢ (𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o} → 𝑘 ∈ 𝐴)
21	10	adantr 483	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ¬ ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = ∪ 𝑧)
22		ssdif0 4323	. . . . . . . . 9 ⊢ (∪ (𝐹‘𝑘) ⊆ ∪ 𝐾 ↔ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾) = ∅)
23	6	ffvelrnda 6851	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐹‘𝑘) ∈ Comp)
24	23	adantr 483	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) → (𝐹‘𝑘) ∈ Comp)
25		ptcmplem3.8	. . . . . . . . . . . . . 14 ⊢ 𝐾 = {𝑢 ∈ (𝐹‘𝑘) ∣ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) ∈ 𝑈}
26	25	ssrab3 4057	. . . . . . . . . . . . 13 ⊢ 𝐾 ⊆ (𝐹‘𝑘)
27	26	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) → 𝐾 ⊆ (𝐹‘𝑘))
28		simpr 487	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) → ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾)
29		uniss 4846	. . . . . . . . . . . . . 14 ⊢ (𝐾 ⊆ (𝐹‘𝑘) → ∪ 𝐾 ⊆ ∪ (𝐹‘𝑘))
30	26, 29	mp1i 13	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) → ∪ 𝐾 ⊆ ∪ (𝐹‘𝑘))
31	28, 30	eqssd 3984	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) → ∪ (𝐹‘𝑘) = ∪ 𝐾)
32		eqid 2821	. . . . . . . . . . . . 13 ⊢ ∪ (𝐹‘𝑘) = ∪ (𝐹‘𝑘)
33	32	cmpcov 21997	. . . . . . . . . . . 12 ⊢ (((𝐹‘𝑘) ∈ Comp ∧ 𝐾 ⊆ (𝐹‘𝑘) ∧ ∪ (𝐹‘𝑘) = ∪ 𝐾) → ∃𝑡 ∈ (𝒫 𝐾 ∩ Fin)∪ (𝐹‘𝑘) = ∪ 𝑡)
34	24, 27, 31, 33	syl3anc 1367	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) → ∃𝑡 ∈ (𝒫 𝐾 ∩ Fin)∪ (𝐹‘𝑘) = ∪ 𝑡)
35		elfpw 8826	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ↔ (𝑡 ⊆ 𝐾 ∧ 𝑡 ∈ Fin))
36	35	simplbi 500	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) → 𝑡 ⊆ 𝐾)
37	36	ad2antrl 726	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → 𝑡 ⊆ 𝐾)
38	37	sselda 3967	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑥 ∈ 𝑡) → 𝑥 ∈ 𝐾)
39		imaeq2 5925	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢 = 𝑥 → (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) = (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥))
40	39	eleq1d 2897	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑢 = 𝑥 → ((◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) ∈ 𝑈 ↔ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) ∈ 𝑈))
41	40, 25	elrab2 3683	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ 𝐾 ↔ (𝑥 ∈ (𝐹‘𝑘) ∧ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) ∈ 𝑈))
42	41	simprbi 499	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ 𝐾 → (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) ∈ 𝑈)
43	38, 42	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑥 ∈ 𝑡) → (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) ∈ 𝑈)
44	43	fmpttd 6879	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)):𝑡⟶𝑈)
45	44	frnd 6521	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) ⊆ 𝑈)
46	35	simprbi 499	. . . . . . . . . . . . . . 15 ⊢ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) → 𝑡 ∈ Fin)
47	46	ad2antrl 726	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → 𝑡 ∈ Fin)
48		eqid 2821	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) = (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥))
49	48	rnmpt 5827	. . . . . . . . . . . . . . 15 ⊢ ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) = {𝑓 ∣ ∃𝑥 ∈ 𝑡 𝑓 = (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)}
50		abrexfi 8824	. . . . . . . . . . . . . . 15 ⊢ (𝑡 ∈ Fin → {𝑓 ∣ ∃𝑥 ∈ 𝑡 𝑓 = (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)} ∈ Fin)
51	49, 50	eqeltrid 2917	. . . . . . . . . . . . . 14 ⊢ (𝑡 ∈ Fin → ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) ∈ Fin)
52	47, 51	syl 17	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) ∈ Fin)
53		elfpw 8826	. . . . . . . . . . . . 13 ⊢ (ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) ∈ (𝒫 𝑈 ∩ Fin) ↔ (ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) ⊆ 𝑈 ∧ ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) ∈ Fin))
54	45, 52, 53	sylanbrc 585	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) ∈ (𝒫 𝑈 ∩ Fin))
55		fveq2 6670	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = 𝑘 → (𝑓‘𝑛) = (𝑓‘𝑘))
56		fveq2 6670	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = 𝑘 → (𝐹‘𝑛) = (𝐹‘𝑘))
57	56	unieqd 4852	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = 𝑘 → ∪ (𝐹‘𝑛) = ∪ (𝐹‘𝑘))
58	55, 57	eleq12d 2907	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝑘 → ((𝑓‘𝑛) ∈ ∪ (𝐹‘𝑛) ↔ (𝑓‘𝑘) ∈ ∪ (𝐹‘𝑘)))
59		simpr 487	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑓 ∈ 𝑋) → 𝑓 ∈ 𝑋)
60	59, 5	eleqtrdi 2923	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑓 ∈ 𝑋) → 𝑓 ∈ X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛))
61		vex 3497	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 𝑓 ∈ V
62	61	elixp 8468	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓 ∈ X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛) ↔ (𝑓 Fn 𝐴 ∧ ∀𝑛 ∈ 𝐴 (𝑓‘𝑛) ∈ ∪ (𝐹‘𝑛)))
63	62	simprbi 499	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓 ∈ X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛) → ∀𝑛 ∈ 𝐴 (𝑓‘𝑛) ∈ ∪ (𝐹‘𝑛))
64	60, 63	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑓 ∈ 𝑋) → ∀𝑛 ∈ 𝐴 (𝑓‘𝑛) ∈ ∪ (𝐹‘𝑛))
65		simp-4r 782	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑓 ∈ 𝑋) → 𝑘 ∈ 𝐴)
66	58, 64, 65	rspcdva 3625	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑓 ∈ 𝑋) → (𝑓‘𝑘) ∈ ∪ (𝐹‘𝑘))
67		simplrr 776	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑓 ∈ 𝑋) → ∪ (𝐹‘𝑘) = ∪ 𝑡)
68	66, 67	eleqtrd 2915	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑓 ∈ 𝑋) → (𝑓‘𝑘) ∈ ∪ 𝑡)
69		eluni2 4842	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓‘𝑘) ∈ ∪ 𝑡 ↔ ∃𝑥 ∈ 𝑡 (𝑓‘𝑘) ∈ 𝑥)
70	68, 69	sylib 220	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑓 ∈ 𝑋) → ∃𝑥 ∈ 𝑡 (𝑓‘𝑘) ∈ 𝑥)
71		fveq1 6669	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = 𝑓 → (𝑤‘𝑘) = (𝑓‘𝑘))
72	71	eleq1d 2897	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 = 𝑓 → ((𝑤‘𝑘) ∈ 𝑥 ↔ (𝑓‘𝑘) ∈ 𝑥))
73		eqid 2821	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) = (𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘))
74	73	mptpreima 6092	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) = {𝑤 ∈ 𝑋 ∣ (𝑤‘𝑘) ∈ 𝑥}
75	72, 74	elrab2 3683	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 ∈ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) ↔ (𝑓 ∈ 𝑋 ∧ (𝑓‘𝑘) ∈ 𝑥))
76	75	baib 538	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 ∈ 𝑋 → (𝑓 ∈ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) ↔ (𝑓‘𝑘) ∈ 𝑥))
77	76	ad2antlr 725	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑓 ∈ 𝑋) ∧ 𝑥 ∈ 𝑡) → (𝑓 ∈ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) ↔ (𝑓‘𝑘) ∈ 𝑥))
78	77	rexbidva 3296	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑓 ∈ 𝑋) → (∃𝑥 ∈ 𝑡 𝑓 ∈ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) ↔ ∃𝑥 ∈ 𝑡 (𝑓‘𝑘) ∈ 𝑥))
79	70, 78	mpbird 259	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑓 ∈ 𝑋) → ∃𝑥 ∈ 𝑡 𝑓 ∈ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥))
80		eliun 4923	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 ∈ ∪ 𝑥 ∈ 𝑡 (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) ↔ ∃𝑥 ∈ 𝑡 𝑓 ∈ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥))
81	79, 80	sylibr 236	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑓 ∈ 𝑋) → 𝑓 ∈ ∪ 𝑥 ∈ 𝑡 (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥))
82	81	ex 415	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → (𝑓 ∈ 𝑋 → 𝑓 ∈ ∪ 𝑥 ∈ 𝑡 (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)))
83	82	ssrdv 3973	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → 𝑋 ⊆ ∪ 𝑥 ∈ 𝑡 (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥))
84	43	ralrimiva 3182	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → ∀𝑥 ∈ 𝑡 (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) ∈ 𝑈)
85		dfiun2g 4955	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑥 ∈ 𝑡 (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) ∈ 𝑈 → ∪ 𝑥 ∈ 𝑡 (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) = ∪ {𝑓 ∣ ∃𝑥 ∈ 𝑡 𝑓 = (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)})
86	84, 85	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → ∪ 𝑥 ∈ 𝑡 (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) = ∪ {𝑓 ∣ ∃𝑥 ∈ 𝑡 𝑓 = (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)})
87	49	unieqi 4851	. . . . . . . . . . . . . . 15 ⊢ ∪ ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) = ∪ {𝑓 ∣ ∃𝑥 ∈ 𝑡 𝑓 = (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)}
88	86, 87	syl6eqr 2874	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → ∪ 𝑥 ∈ 𝑡 (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) = ∪ ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)))
89	83, 88	sseqtrd 4007	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → 𝑋 ⊆ ∪ ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)))
90	45	unissd 4848	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → ∪ ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) ⊆ ∪ 𝑈)
91	9	ad3antrrr 728	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → 𝑋 = ∪ 𝑈)
92	90, 91	sseqtrrd 4008	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → ∪ ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) ⊆ 𝑋)
93	89, 92	eqssd 3984	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → 𝑋 = ∪ ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)))
94		unieq 4849	. . . . . . . . . . . . 13 ⊢ (𝑧 = ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) → ∪ 𝑧 = ∪ ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)))
95	94	rspceeqv 3638	. . . . . . . . . . . 12 ⊢ ((ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑋 = ∪ ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥))) → ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = ∪ 𝑧)
96	54, 93, 95	syl2anc 586	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = ∪ 𝑧)
97	34, 96	rexlimddv 3291	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) → ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = ∪ 𝑧)
98	97	ex 415	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (∪ (𝐹‘𝑘) ⊆ ∪ 𝐾 → ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = ∪ 𝑧))
99	22, 98	syl5bir 245	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((∪ (𝐹‘𝑘) ∖ ∪ 𝐾) = ∅ → ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = ∪ 𝑧))
100	21, 99	mtod 200	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ¬ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾) = ∅)
101		neq0 4309	. . . . . . 7 ⊢ (¬ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾) = ∅ ↔ ∃𝑦 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))
102	100, 101	sylib 220	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ∃𝑦 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))
103		rexv 3520	. . . . . 6 ⊢ (∃𝑦 ∈ V 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾) ↔ ∃𝑦 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))
104	102, 103	sylibr 236	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ∃𝑦 ∈ V 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))
105	20, 104	sylan2 594	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}) → ∃𝑦 ∈ V 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))
106	105	ralrimiva 3182	. . 3 ⊢ (𝜑 → ∀𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}∃𝑦 ∈ V 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))
107		eleq1 2900	. . . 4 ⊢ (𝑦 = (𝑔‘𝑘) → (𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾) ↔ (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)))
108	107	ac6num 9901	. . 3 ⊢ (({𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o} ∈ V ∧ ∪ 𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o} {𝑦 ∈ V ∣ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)} ∈ dom card ∧ ∀𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}∃𝑦 ∈ V 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → ∃𝑔(𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}⟶V ∧ ∀𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o} (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)))
109	3, 19, 106, 108	syl3anc 1367	. 2 ⊢ (𝜑 → ∃𝑔(𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}⟶V ∧ ∀𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o} (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)))
110	1	adantr 483	. . . 4 ⊢ ((𝜑 ∧ (𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}⟶V ∧ ∀𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o} (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))) → 𝐴 ∈ 𝑉)
111	110	mptexd 6987	. . 3 ⊢ ((𝜑 ∧ (𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}⟶V ∧ ∀𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o} (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))) → (𝑚 ∈ 𝐴 ↦ if(∪ (𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) ∈ V)
112		fvex 6683	. . . . . . . 8 ⊢ (𝐹‘𝑚) ∈ V
113	112	uniex 7467	. . . . . . 7 ⊢ ∪ (𝐹‘𝑚) ∈ V
114	113	uniex 7467	. . . . . 6 ⊢ ∪ ∪ (𝐹‘𝑚) ∈ V
115		fvex 6683	. . . . . 6 ⊢ (𝑔‘𝑚) ∈ V
116	114, 115	ifex 4515	. . . . 5 ⊢ if(∪ (𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚)) ∈ V
117	116	rgenw 3150	. . . 4 ⊢ ∀𝑚 ∈ 𝐴 if(∪ (𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚)) ∈ V
118		eqid 2821	. . . . 5 ⊢ (𝑚 ∈ 𝐴 ↦ if(∪ (𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) = (𝑚 ∈ 𝐴 ↦ if(∪ (𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚)))
119	118	fnmpt 6488	. . . 4 ⊢ (∀𝑚 ∈ 𝐴 if(∪ (𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚)) ∈ V → (𝑚 ∈ 𝐴 ↦ if(∪ (𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) Fn 𝐴)
120	117, 119	mp1i 13	. . 3 ⊢ ((𝜑 ∧ (𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}⟶V ∧ ∀𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o} (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))) → (𝑚 ∈ 𝐴 ↦ if(∪ (𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) Fn 𝐴)
121	57	breq1d 5076	. . . . . . 7 ⊢ (𝑛 = 𝑘 → (∪ (𝐹‘𝑛) ≈ 1o ↔ ∪ (𝐹‘𝑘) ≈ 1o))
122	121	notbid 320	. . . . . 6 ⊢ (𝑛 = 𝑘 → (¬ ∪ (𝐹‘𝑛) ≈ 1o ↔ ¬ ∪ (𝐹‘𝑘) ≈ 1o))
123	122	ralrab 3685	. . . . 5 ⊢ (∀𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o} (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾) ↔ ∀𝑘 ∈ 𝐴 (¬ ∪ (𝐹‘𝑘) ≈ 1o → (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)))
124		iftrue 4473	. . . . . . . . . . 11 ⊢ (∪ (𝐹‘𝑘) ≈ 1o → if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) = ∪ ∪ (𝐹‘𝑘))
125	124	ad2antll 727	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}⟶V) ∧ (𝑘 ∈ 𝐴 ∧ ∪ (𝐹‘𝑘) ≈ 1o)) → if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) = ∪ ∪ (𝐹‘𝑘))
126	102	adantrr 715	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑘 ∈ 𝐴 ∧ ∪ (𝐹‘𝑘) ≈ 1o)) → ∃𝑦 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))
127	12	adantl 484	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑘 ∈ 𝐴 ∧ ∪ (𝐹‘𝑘) ≈ 1o)) ∧ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → 𝑦 ∈ ∪ (𝐹‘𝑘))
128		simplrr 776	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑘 ∈ 𝐴 ∧ ∪ (𝐹‘𝑘) ≈ 1o)) ∧ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → ∪ (𝐹‘𝑘) ≈ 1o)
129		en1b 8577	. . . . . . . . . . . . . . . 16 ⊢ (∪ (𝐹‘𝑘) ≈ 1o ↔ ∪ (𝐹‘𝑘) = {∪ ∪ (𝐹‘𝑘)})
130	128, 129	sylib 220	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑘 ∈ 𝐴 ∧ ∪ (𝐹‘𝑘) ≈ 1o)) ∧ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → ∪ (𝐹‘𝑘) = {∪ ∪ (𝐹‘𝑘)})
131	127, 130	eleqtrd 2915	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑘 ∈ 𝐴 ∧ ∪ (𝐹‘𝑘) ≈ 1o)) ∧ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → 𝑦 ∈ {∪ ∪ (𝐹‘𝑘)})
132		elsni 4584	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ {∪ ∪ (𝐹‘𝑘)} → 𝑦 = ∪ ∪ (𝐹‘𝑘))
133	131, 132	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑘 ∈ 𝐴 ∧ ∪ (𝐹‘𝑘) ≈ 1o)) ∧ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → 𝑦 = ∪ ∪ (𝐹‘𝑘))
134		simpr 487	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑘 ∈ 𝐴 ∧ ∪ (𝐹‘𝑘) ≈ 1o)) ∧ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))
135	133, 134	eqeltrrd 2914	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑘 ∈ 𝐴 ∧ ∪ (𝐹‘𝑘) ≈ 1o)) ∧ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → ∪ ∪ (𝐹‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))
136	126, 135	exlimddv 1936	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑘 ∈ 𝐴 ∧ ∪ (𝐹‘𝑘) ≈ 1o)) → ∪ ∪ (𝐹‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))
137	136	adantlr 713	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}⟶V) ∧ (𝑘 ∈ 𝐴 ∧ ∪ (𝐹‘𝑘) ≈ 1o)) → ∪ ∪ (𝐹‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))
138	125, 137	eqeltrd 2913	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}⟶V) ∧ (𝑘 ∈ 𝐴 ∧ ∪ (𝐹‘𝑘) ≈ 1o)) → if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))
139	138	a1d 25	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}⟶V) ∧ (𝑘 ∈ 𝐴 ∧ ∪ (𝐹‘𝑘) ≈ 1o)) → ((¬ ∪ (𝐹‘𝑘) ≈ 1o → (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)))
140	139	expr 459	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}⟶V) ∧ 𝑘 ∈ 𝐴) → (∪ (𝐹‘𝑘) ≈ 1o → ((¬ ∪ (𝐹‘𝑘) ≈ 1o → (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))))
141		pm2.27 42	. . . . . . . 8 ⊢ (¬ ∪ (𝐹‘𝑘) ≈ 1o → ((¬ ∪ (𝐹‘𝑘) ≈ 1o → (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)))
142		iffalse 4476	. . . . . . . . 9 ⊢ (¬ ∪ (𝐹‘𝑘) ≈ 1o → if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) = (𝑔‘𝑘))
143	142	eleq1d 2897	. . . . . . . 8 ⊢ (¬ ∪ (𝐹‘𝑘) ≈ 1o → (if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾) ↔ (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)))
144	141, 143	sylibrd 261	. . . . . . 7 ⊢ (¬ ∪ (𝐹‘𝑘) ≈ 1o → ((¬ ∪ (𝐹‘𝑘) ≈ 1o → (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)))
145	140, 144	pm2.61d1 182	. . . . . 6 ⊢ (((𝜑 ∧ 𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}⟶V) ∧ 𝑘 ∈ 𝐴) → ((¬ ∪ (𝐹‘𝑘) ≈ 1o → (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)))
146	145	ralimdva 3177	. . . . 5 ⊢ ((𝜑 ∧ 𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}⟶V) → (∀𝑘 ∈ 𝐴 (¬ ∪ (𝐹‘𝑘) ≈ 1o → (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → ∀𝑘 ∈ 𝐴 if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)))
147	123, 146	syl5bi 244	. . . 4 ⊢ ((𝜑 ∧ 𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}⟶V) → (∀𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o} (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾) → ∀𝑘 ∈ 𝐴 if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)))
148	147	impr 457	. . 3 ⊢ ((𝜑 ∧ (𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}⟶V ∧ ∀𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o} (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))) → ∀𝑘 ∈ 𝐴 if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))
149		fneq1 6444	. . . . . 6 ⊢ (𝑓 = (𝑚 ∈ 𝐴 ↦ if(∪ (𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) → (𝑓 Fn 𝐴 ↔ (𝑚 ∈ 𝐴 ↦ if(∪ (𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) Fn 𝐴))
150		fveq1 6669	. . . . . . . . 9 ⊢ (𝑓 = (𝑚 ∈ 𝐴 ↦ if(∪ (𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) → (𝑓‘𝑘) = ((𝑚 ∈ 𝐴 ↦ if(∪ (𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚)))‘𝑘))
151		fveq2 6670	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑘 → (𝐹‘𝑚) = (𝐹‘𝑘))
152	151	unieqd 4852	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑘 → ∪ (𝐹‘𝑚) = ∪ (𝐹‘𝑘))
153	152	breq1d 5076	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑘 → (∪ (𝐹‘𝑚) ≈ 1o ↔ ∪ (𝐹‘𝑘) ≈ 1o))
154	152	unieqd 4852	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑘 → ∪ ∪ (𝐹‘𝑚) = ∪ ∪ (𝐹‘𝑘))
155		fveq2 6670	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑘 → (𝑔‘𝑚) = (𝑔‘𝑘))
156	153, 154, 155	ifbieq12d 4494	. . . . . . . . . 10 ⊢ (𝑚 = 𝑘 → if(∪ (𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚)) = if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)))
157		fvex 6683	. . . . . . . . . . . . 13 ⊢ (𝐹‘𝑘) ∈ V
158	157	uniex 7467	. . . . . . . . . . . 12 ⊢ ∪ (𝐹‘𝑘) ∈ V
159	158	uniex 7467	. . . . . . . . . . 11 ⊢ ∪ ∪ (𝐹‘𝑘) ∈ V
160		fvex 6683	. . . . . . . . . . 11 ⊢ (𝑔‘𝑘) ∈ V
161	159, 160	ifex 4515	. . . . . . . . . 10 ⊢ if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ V
162	156, 118, 161	fvmpt 6768	. . . . . . . . 9 ⊢ (𝑘 ∈ 𝐴 → ((𝑚 ∈ 𝐴 ↦ if(∪ (𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚)))‘𝑘) = if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)))
163	150, 162	sylan9eq 2876	. . . . . . . 8 ⊢ ((𝑓 = (𝑚 ∈ 𝐴 ↦ if(∪ (𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) ∧ 𝑘 ∈ 𝐴) → (𝑓‘𝑘) = if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)))
164	163	eleq1d 2897	. . . . . . 7 ⊢ ((𝑓 = (𝑚 ∈ 𝐴 ↦ if(∪ (𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) ∧ 𝑘 ∈ 𝐴) → ((𝑓‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾) ↔ if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)))
165	164	ralbidva 3196	. . . . . 6 ⊢ (𝑓 = (𝑚 ∈ 𝐴 ↦ if(∪ (𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) → (∀𝑘 ∈ 𝐴 (𝑓‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾) ↔ ∀𝑘 ∈ 𝐴 if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)))
166	149, 165	anbi12d 632	. . . . 5 ⊢ (𝑓 = (𝑚 ∈ 𝐴 ↦ if(∪ (𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) → ((𝑓 Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (𝑓‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) ↔ ((𝑚 ∈ 𝐴 ↦ if(∪ (𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))))
167	166	spcegv 3597	. . . 4 ⊢ ((𝑚 ∈ 𝐴 ↦ if(∪ (𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) ∈ V → (((𝑚 ∈ 𝐴 ↦ if(∪ (𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (𝑓‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))))
168	167	3impib 1112	. . 3 ⊢ (((𝑚 ∈ 𝐴 ↦ if(∪ (𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) ∈ V ∧ (𝑚 ∈ 𝐴 ↦ if(∪ (𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (𝑓‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)))
169	111, 120, 148, 168	syl3anc 1367	. 2 ⊢ ((𝜑 ∧ (𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}⟶V ∧ ∀𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o} (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))) → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (𝑓‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)))
170	109, 169	exlimddv 1936	1 ⊢ (𝜑 → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (𝑓‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1537  ∃wex 1780   ∈ wcel 2114  {cab 2799  ∀wral 3138  ∃wrex 3139  {crab 3142  Vcvv 3494   ∖ cdif 3933   ∩ cin 3935   ⊆ wss 3936  ∅c0 4291  ifcif 4467  𝒫 cpw 4539  {csn 4567  ∪ cuni 4838  ∪ ciun 4919   class class class wbr 5066   ↦ cmpt 5146  ^◡ccnv 5554  dom cdm 5555  ran crn 5556   “ cima 5558   Fn wfn 6350  ⟶wf 6351  ‘cfv 6355   ∈ cmpo 7158  1_oc1o 8095  Xcixp 8461   ≈ cen 8506  Fincfn 8509  cardccrd 9364  Compccmp 21994  UFLcufl 22508

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-rep 5190  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330  ax-un 7461

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-reu 3145  df-rmo 3146  df-rab 3147  df-v 3496  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-pss 3954  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-tp 4572  df-op 4574  df-uni 4839  df-int 4877  df-iun 4921  df-br 5067  df-opab 5129  df-mpt 5147  df-tr 5173  df-id 5460  df-eprel 5465  df-po 5474  df-so 5475  df-fr 5514  df-se 5515  df-we 5516  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-pred 6148  df-ord 6194  df-on 6195  df-lim 6196  df-suc 6197  df-iota 6314  df-fun 6357  df-fn 6358  df-f 6359  df-f1 6360  df-fo 6361  df-f1o 6362  df-fv 6363  df-isom 6364  df-riota 7114  df-ov 7159  df-oprab 7160  df-mpo 7161  df-om 7581  df-1st 7689  df-2nd 7690  df-wrecs 7947  df-recs 8008  df-rdg 8046  df-1o 8102  df-oadd 8106  df-omul 8107  df-er 8289  df-map 8408  df-ixp 8462  df-en 8510  df-dom 8511  df-fin 8513  df-wdom 9023  df-card 9368  df-acn 9371  df-cmp 21995

This theorem is referenced by:  ptcmplem4  22663