Theorem ptcmplem3 22659

Description: Lemma for ptcmp 22663. (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 5198	. . . 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 22658	. . . 4 ⊢ (𝜑 → ∪ 𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}∪ (𝐹‘𝑘) ∈ dom card)
12		eldifi 4054	. . . . . . . 8 ⊢ (𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾) → 𝑦 ∈ ∪ (𝐹‘𝑘))
13	12	3ad2ant3 1132	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ V ∧ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → 𝑦 ∈ ∪ (𝐹‘𝑘))
14	13	rabssdv 4002	. . . . . 6 ⊢ (𝜑 → {𝑦 ∈ V ∣ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)} ⊆ ∪ (𝐹‘𝑘))
15	14	ralrimivw 3150	. . . . 5 ⊢ (𝜑 → ∀𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o} {𝑦 ∈ V ∣ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)} ⊆ ∪ (𝐹‘𝑘))
16		ss2iun 4899	. . . . 5 ⊢ (∀𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o} {𝑦 ∈ V ∣ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)} ⊆ ∪ (𝐹‘𝑘) → ∪ 𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o} {𝑦 ∈ V ∣ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)} ⊆ ∪ 𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}∪ (𝐹‘𝑘))
17	15, 16	syl 17	. . . 4 ⊢ (𝜑 → ∪ 𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o} {𝑦 ∈ V ∣ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)} ⊆ ∪ 𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}∪ (𝐹‘𝑘))
18		ssnum 9450	. . . 4 ⊢ ((∪ 𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}∪ (𝐹‘𝑘) ∈ dom card ∧ ∪ 𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o} {𝑦 ∈ V ∣ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)} ⊆ ∪ 𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}∪ (𝐹‘𝑘)) → ∪ 𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o} {𝑦 ∈ V ∣ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)} ∈ dom card)
19	11, 17, 18	syl2anc 587	. . 3 ⊢ (𝜑 → ∪ 𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o} {𝑦 ∈ V ∣ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)} ∈ dom card)
20		elrabi 3623	. . . . 5 ⊢ (𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o} → 𝑘 ∈ 𝐴)
21	10	adantr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ¬ ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = ∪ 𝑧)
22		ssdif0 4277	. . . . . . . . 9 ⊢ (∪ (𝐹‘𝑘) ⊆ ∪ 𝐾 ↔ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾) = ∅)
23	6	ffvelrnda 6828	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐹‘𝑘) ∈ Comp)
24	23	adantr 484	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) → (𝐹‘𝑘) ∈ Comp)
25		ptcmplem3.8	. . . . . . . . . . . . . 14 ⊢ 𝐾 = {𝑢 ∈ (𝐹‘𝑘) ∣ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) ∈ 𝑈}
26	25	ssrab3 4008	. . . . . . . . . . . . 13 ⊢ 𝐾 ⊆ (𝐹‘𝑘)
27	26	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) → 𝐾 ⊆ (𝐹‘𝑘))
28		simpr 488	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) → ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾)
29		uniss 4808	. . . . . . . . . . . . . 14 ⊢ (𝐾 ⊆ (𝐹‘𝑘) → ∪ 𝐾 ⊆ ∪ (𝐹‘𝑘))
30	26, 29	mp1i 13	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) → ∪ 𝐾 ⊆ ∪ (𝐹‘𝑘))
31	28, 30	eqssd 3932	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) → ∪ (𝐹‘𝑘) = ∪ 𝐾)
32		eqid 2798	. . . . . . . . . . . . 13 ⊢ ∪ (𝐹‘𝑘) = ∪ (𝐹‘𝑘)
33	32	cmpcov 21994	. . . . . . . . . . . 12 ⊢ (((𝐹‘𝑘) ∈ Comp ∧ 𝐾 ⊆ (𝐹‘𝑘) ∧ ∪ (𝐹‘𝑘) = ∪ 𝐾) → ∃𝑡 ∈ (𝒫 𝐾 ∩ Fin)∪ (𝐹‘𝑘) = ∪ 𝑡)
34	24, 27, 31, 33	syl3anc 1368	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) → ∃𝑡 ∈ (𝒫 𝐾 ∩ Fin)∪ (𝐹‘𝑘) = ∪ 𝑡)
35		elfpw 8810	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ↔ (𝑡 ⊆ 𝐾 ∧ 𝑡 ∈ Fin))
36	35	simplbi 501	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) → 𝑡 ⊆ 𝐾)
37	36	ad2antrl 727	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → 𝑡 ⊆ 𝐾)
38	37	sselda 3915	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑥 ∈ 𝑡) → 𝑥 ∈ 𝐾)
39		imaeq2 5892	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢 = 𝑥 → (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) = (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥))
40	39	eleq1d 2874	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑢 = 𝑥 → ((◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) ∈ 𝑈 ↔ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) ∈ 𝑈))
41	40, 25	elrab2 3631	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ 𝐾 ↔ (𝑥 ∈ (𝐹‘𝑘) ∧ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) ∈ 𝑈))
42	41	simprbi 500	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ 𝐾 → (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) ∈ 𝑈)
43	38, 42	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑥 ∈ 𝑡) → (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) ∈ 𝑈)
44	43	fmpttd 6856	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)):𝑡⟶𝑈)
45	44	frnd 6494	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) ⊆ 𝑈)
46	35	simprbi 500	. . . . . . . . . . . . . . 15 ⊢ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) → 𝑡 ∈ Fin)
47	46	ad2antrl 727	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → 𝑡 ∈ Fin)
48		eqid 2798	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) = (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥))
49	48	rnmpt 5791	. . . . . . . . . . . . . . 15 ⊢ ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) = {𝑓 ∣ ∃𝑥 ∈ 𝑡 𝑓 = (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)}
50		abrexfi 8808	. . . . . . . . . . . . . . 15 ⊢ (𝑡 ∈ Fin → {𝑓 ∣ ∃𝑥 ∈ 𝑡 𝑓 = (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)} ∈ Fin)
51	49, 50	eqeltrid 2894	. . . . . . . . . . . . . 14 ⊢ (𝑡 ∈ Fin → ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) ∈ Fin)
52	47, 51	syl 17	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) ∈ Fin)
53		elfpw 8810	. . . . . . . . . . . . 13 ⊢ (ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) ∈ (𝒫 𝑈 ∩ Fin) ↔ (ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) ⊆ 𝑈 ∧ ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) ∈ Fin))
54	45, 52, 53	sylanbrc 586	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) ∈ (𝒫 𝑈 ∩ Fin))
55		fveq2 6645	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = 𝑘 → (𝑓‘𝑛) = (𝑓‘𝑘))
56		fveq2 6645	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = 𝑘 → (𝐹‘𝑛) = (𝐹‘𝑘))
57	56	unieqd 4814	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = 𝑘 → ∪ (𝐹‘𝑛) = ∪ (𝐹‘𝑘))
58	55, 57	eleq12d 2884	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝑘 → ((𝑓‘𝑛) ∈ ∪ (𝐹‘𝑛) ↔ (𝑓‘𝑘) ∈ ∪ (𝐹‘𝑘)))
59		simpr 488	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑓 ∈ 𝑋) → 𝑓 ∈ 𝑋)
60	59, 5	eleqtrdi 2900	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑓 ∈ 𝑋) → 𝑓 ∈ X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛))
61		vex 3444	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 𝑓 ∈ V
62	61	elixp 8451	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓 ∈ X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛) ↔ (𝑓 Fn 𝐴 ∧ ∀𝑛 ∈ 𝐴 (𝑓‘𝑛) ∈ ∪ (𝐹‘𝑛)))
63	62	simprbi 500	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓 ∈ X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛) → ∀𝑛 ∈ 𝐴 (𝑓‘𝑛) ∈ ∪ (𝐹‘𝑛))
64	60, 63	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑓 ∈ 𝑋) → ∀𝑛 ∈ 𝐴 (𝑓‘𝑛) ∈ ∪ (𝐹‘𝑛))
65		simp-4r 783	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑓 ∈ 𝑋) → 𝑘 ∈ 𝐴)
66	58, 64, 65	rspcdva 3573	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑓 ∈ 𝑋) → (𝑓‘𝑘) ∈ ∪ (𝐹‘𝑘))
67		simplrr 777	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑓 ∈ 𝑋) → ∪ (𝐹‘𝑘) = ∪ 𝑡)
68	66, 67	eleqtrd 2892	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑓 ∈ 𝑋) → (𝑓‘𝑘) ∈ ∪ 𝑡)
69		eluni2 4804	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓‘𝑘) ∈ ∪ 𝑡 ↔ ∃𝑥 ∈ 𝑡 (𝑓‘𝑘) ∈ 𝑥)
70	68, 69	sylib 221	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑓 ∈ 𝑋) → ∃𝑥 ∈ 𝑡 (𝑓‘𝑘) ∈ 𝑥)
71		fveq1 6644	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = 𝑓 → (𝑤‘𝑘) = (𝑓‘𝑘))
72	71	eleq1d 2874	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 = 𝑓 → ((𝑤‘𝑘) ∈ 𝑥 ↔ (𝑓‘𝑘) ∈ 𝑥))
73		eqid 2798	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) = (𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘))
74	73	mptpreima 6059	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) = {𝑤 ∈ 𝑋 ∣ (𝑤‘𝑘) ∈ 𝑥}
75	72, 74	elrab2 3631	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 ∈ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) ↔ (𝑓 ∈ 𝑋 ∧ (𝑓‘𝑘) ∈ 𝑥))
76	75	baib 539	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 ∈ 𝑋 → (𝑓 ∈ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) ↔ (𝑓‘𝑘) ∈ 𝑥))
77	76	ad2antlr 726	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑓 ∈ 𝑋) ∧ 𝑥 ∈ 𝑡) → (𝑓 ∈ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) ↔ (𝑓‘𝑘) ∈ 𝑥))
78	77	rexbidva 3255	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑓 ∈ 𝑋) → (∃𝑥 ∈ 𝑡 𝑓 ∈ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) ↔ ∃𝑥 ∈ 𝑡 (𝑓‘𝑘) ∈ 𝑥))
79	70, 78	mpbird 260	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑓 ∈ 𝑋) → ∃𝑥 ∈ 𝑡 𝑓 ∈ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥))
80		eliun 4885	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 ∈ ∪ 𝑥 ∈ 𝑡 (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) ↔ ∃𝑥 ∈ 𝑡 𝑓 ∈ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥))
81	79, 80	sylibr 237	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑓 ∈ 𝑋) → 𝑓 ∈ ∪ 𝑥 ∈ 𝑡 (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥))
82	81	ex 416	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → (𝑓 ∈ 𝑋 → 𝑓 ∈ ∪ 𝑥 ∈ 𝑡 (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)))
83	82	ssrdv 3921	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → 𝑋 ⊆ ∪ 𝑥 ∈ 𝑡 (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥))
84	43	ralrimiva 3149	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → ∀𝑥 ∈ 𝑡 (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) ∈ 𝑈)
85		dfiun2g 4917	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑥 ∈ 𝑡 (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) ∈ 𝑈 → ∪ 𝑥 ∈ 𝑡 (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) = ∪ {𝑓 ∣ ∃𝑥 ∈ 𝑡 𝑓 = (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)})
86	84, 85	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → ∪ 𝑥 ∈ 𝑡 (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) = ∪ {𝑓 ∣ ∃𝑥 ∈ 𝑡 𝑓 = (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)})
87	49	unieqi 4813	. . . . . . . . . . . . . . 15 ⊢ ∪ ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) = ∪ {𝑓 ∣ ∃𝑥 ∈ 𝑡 𝑓 = (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)}
88	86, 87	eqtr4di 2851	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → ∪ 𝑥 ∈ 𝑡 (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) = ∪ ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)))
89	83, 88	sseqtrd 3955	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → 𝑋 ⊆ ∪ ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)))
90	45	unissd 4810	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → ∪ ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) ⊆ ∪ 𝑈)
91	9	ad3antrrr 729	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → 𝑋 = ∪ 𝑈)
92	90, 91	sseqtrrd 3956	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → ∪ ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) ⊆ 𝑋)
93	89, 92	eqssd 3932	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → 𝑋 = ∪ ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)))
94		unieq 4811	. . . . . . . . . . . . 13 ⊢ (𝑧 = ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) → ∪ 𝑧 = ∪ ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)))
95	94	rspceeqv 3586	. . . . . . . . . . . 12 ⊢ ((ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑋 = ∪ ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥))) → ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = ∪ 𝑧)
96	54, 93, 95	syl2anc 587	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = ∪ 𝑧)
97	34, 96	rexlimddv 3250	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) → ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = ∪ 𝑧)
98	97	ex 416	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (∪ (𝐹‘𝑘) ⊆ ∪ 𝐾 → ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = ∪ 𝑧))
99	22, 98	syl5bir 246	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((∪ (𝐹‘𝑘) ∖ ∪ 𝐾) = ∅ → ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = ∪ 𝑧))
100	21, 99	mtod 201	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ¬ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾) = ∅)
101		neq0 4259	. . . . . . 7 ⊢ (¬ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾) = ∅ ↔ ∃𝑦 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))
102	100, 101	sylib 221	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ∃𝑦 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))
103		rexv 3467	. . . . . 6 ⊢ (∃𝑦 ∈ V 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾) ↔ ∃𝑦 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))
104	102, 103	sylibr 237	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ∃𝑦 ∈ V 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))
105	20, 104	sylan2 595	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}) → ∃𝑦 ∈ V 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))
106	105	ralrimiva 3149	. . 3 ⊢ (𝜑 → ∀𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}∃𝑦 ∈ V 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))
107		eleq1 2877	. . . 4 ⊢ (𝑦 = (𝑔‘𝑘) → (𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾) ↔ (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)))
108	107	ac6num 9890	. . 3 ⊢ (({𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o} ∈ V ∧ ∪ 𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o} {𝑦 ∈ V ∣ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)} ∈ dom card ∧ ∀𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}∃𝑦 ∈ V 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → ∃𝑔(𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}⟶V ∧ ∀𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o} (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)))
109	3, 19, 106, 108	syl3anc 1368	. 2 ⊢ (𝜑 → ∃𝑔(𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}⟶V ∧ ∀𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o} (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)))
110	1	adantr 484	. . . 4 ⊢ ((𝜑 ∧ (𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}⟶V ∧ ∀𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o} (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))) → 𝐴 ∈ 𝑉)
111	110	mptexd 6964	. . 3 ⊢ ((𝜑 ∧ (𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}⟶V ∧ ∀𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o} (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))) → (𝑚 ∈ 𝐴 ↦ if(∪ (𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) ∈ V)
112		fvex 6658	. . . . . . . 8 ⊢ (𝐹‘𝑚) ∈ V
113	112	uniex 7447	. . . . . . 7 ⊢ ∪ (𝐹‘𝑚) ∈ V
114	113	uniex 7447	. . . . . 6 ⊢ ∪ ∪ (𝐹‘𝑚) ∈ V
115		fvex 6658	. . . . . 6 ⊢ (𝑔‘𝑚) ∈ V
116	114, 115	ifex 4473	. . . . 5 ⊢ if(∪ (𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚)) ∈ V
117	116	rgenw 3118	. . . 4 ⊢ ∀𝑚 ∈ 𝐴 if(∪ (𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚)) ∈ V
118		eqid 2798	. . . . 5 ⊢ (𝑚 ∈ 𝐴 ↦ if(∪ (𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) = (𝑚 ∈ 𝐴 ↦ if(∪ (𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚)))
119	118	fnmpt 6460	. . . 4 ⊢ (∀𝑚 ∈ 𝐴 if(∪ (𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚)) ∈ V → (𝑚 ∈ 𝐴 ↦ if(∪ (𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) Fn 𝐴)
120	117, 119	mp1i 13	. . 3 ⊢ ((𝜑 ∧ (𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}⟶V ∧ ∀𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o} (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))) → (𝑚 ∈ 𝐴 ↦ if(∪ (𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) Fn 𝐴)
121	57	breq1d 5040	. . . . . . 7 ⊢ (𝑛 = 𝑘 → (∪ (𝐹‘𝑛) ≈ 1o ↔ ∪ (𝐹‘𝑘) ≈ 1o))
122	121	notbid 321	. . . . . 6 ⊢ (𝑛 = 𝑘 → (¬ ∪ (𝐹‘𝑛) ≈ 1o ↔ ¬ ∪ (𝐹‘𝑘) ≈ 1o))
123	122	ralrab 3633	. . . . 5 ⊢ (∀𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o} (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾) ↔ ∀𝑘 ∈ 𝐴 (¬ ∪ (𝐹‘𝑘) ≈ 1o → (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)))
124		iftrue 4431	. . . . . . . . . . 11 ⊢ (∪ (𝐹‘𝑘) ≈ 1o → if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) = ∪ ∪ (𝐹‘𝑘))
125	124	ad2antll 728	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}⟶V) ∧ (𝑘 ∈ 𝐴 ∧ ∪ (𝐹‘𝑘) ≈ 1o)) → if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) = ∪ ∪ (𝐹‘𝑘))
126	102	adantrr 716	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑘 ∈ 𝐴 ∧ ∪ (𝐹‘𝑘) ≈ 1o)) → ∃𝑦 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))
127	12	adantl 485	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑘 ∈ 𝐴 ∧ ∪ (𝐹‘𝑘) ≈ 1o)) ∧ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → 𝑦 ∈ ∪ (𝐹‘𝑘))
128		simplrr 777	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑘 ∈ 𝐴 ∧ ∪ (𝐹‘𝑘) ≈ 1o)) ∧ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → ∪ (𝐹‘𝑘) ≈ 1o)
129		en1b 8560	. . . . . . . . . . . . . . . 16 ⊢ (∪ (𝐹‘𝑘) ≈ 1o ↔ ∪ (𝐹‘𝑘) = {∪ ∪ (𝐹‘𝑘)})
130	128, 129	sylib 221	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑘 ∈ 𝐴 ∧ ∪ (𝐹‘𝑘) ≈ 1o)) ∧ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → ∪ (𝐹‘𝑘) = {∪ ∪ (𝐹‘𝑘)})
131	127, 130	eleqtrd 2892	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑘 ∈ 𝐴 ∧ ∪ (𝐹‘𝑘) ≈ 1o)) ∧ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → 𝑦 ∈ {∪ ∪ (𝐹‘𝑘)})
132		elsni 4542	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ {∪ ∪ (𝐹‘𝑘)} → 𝑦 = ∪ ∪ (𝐹‘𝑘))
133	131, 132	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑘 ∈ 𝐴 ∧ ∪ (𝐹‘𝑘) ≈ 1o)) ∧ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → 𝑦 = ∪ ∪ (𝐹‘𝑘))
134		simpr 488	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑘 ∈ 𝐴 ∧ ∪ (𝐹‘𝑘) ≈ 1o)) ∧ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))
135	133, 134	eqeltrrd 2891	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑘 ∈ 𝐴 ∧ ∪ (𝐹‘𝑘) ≈ 1o)) ∧ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → ∪ ∪ (𝐹‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))
136	126, 135	exlimddv 1936	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑘 ∈ 𝐴 ∧ ∪ (𝐹‘𝑘) ≈ 1o)) → ∪ ∪ (𝐹‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))
137	136	adantlr 714	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}⟶V) ∧ (𝑘 ∈ 𝐴 ∧ ∪ (𝐹‘𝑘) ≈ 1o)) → ∪ ∪ (𝐹‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))
138	125, 137	eqeltrd 2890	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}⟶V) ∧ (𝑘 ∈ 𝐴 ∧ ∪ (𝐹‘𝑘) ≈ 1o)) → if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))
139	138	a1d 25	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}⟶V) ∧ (𝑘 ∈ 𝐴 ∧ ∪ (𝐹‘𝑘) ≈ 1o)) → ((¬ ∪ (𝐹‘𝑘) ≈ 1o → (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)))
140	139	expr 460	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}⟶V) ∧ 𝑘 ∈ 𝐴) → (∪ (𝐹‘𝑘) ≈ 1o → ((¬ ∪ (𝐹‘𝑘) ≈ 1o → (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))))
141		pm2.27 42	. . . . . . . 8 ⊢ (¬ ∪ (𝐹‘𝑘) ≈ 1o → ((¬ ∪ (𝐹‘𝑘) ≈ 1o → (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)))
142		iffalse 4434	. . . . . . . . 9 ⊢ (¬ ∪ (𝐹‘𝑘) ≈ 1o → if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) = (𝑔‘𝑘))
143	142	eleq1d 2874	. . . . . . . 8 ⊢ (¬ ∪ (𝐹‘𝑘) ≈ 1o → (if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾) ↔ (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)))
144	141, 143	sylibrd 262	. . . . . . 7 ⊢ (¬ ∪ (𝐹‘𝑘) ≈ 1o → ((¬ ∪ (𝐹‘𝑘) ≈ 1o → (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)))
145	140, 144	pm2.61d1 183	. . . . . 6 ⊢ (((𝜑 ∧ 𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}⟶V) ∧ 𝑘 ∈ 𝐴) → ((¬ ∪ (𝐹‘𝑘) ≈ 1o → (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)))
146	145	ralimdva 3144	. . . . 5 ⊢ ((𝜑 ∧ 𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}⟶V) → (∀𝑘 ∈ 𝐴 (¬ ∪ (𝐹‘𝑘) ≈ 1o → (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → ∀𝑘 ∈ 𝐴 if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)))
147	123, 146	syl5bi 245	. . . 4 ⊢ ((𝜑 ∧ 𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}⟶V) → (∀𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o} (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾) → ∀𝑘 ∈ 𝐴 if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)))
148	147	impr 458	. . 3 ⊢ ((𝜑 ∧ (𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}⟶V ∧ ∀𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o} (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))) → ∀𝑘 ∈ 𝐴 if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))
149		fneq1 6414	. . . . . 6 ⊢ (𝑓 = (𝑚 ∈ 𝐴 ↦ if(∪ (𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) → (𝑓 Fn 𝐴 ↔ (𝑚 ∈ 𝐴 ↦ if(∪ (𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) Fn 𝐴))
150		fveq1 6644	. . . . . . . . 9 ⊢ (𝑓 = (𝑚 ∈ 𝐴 ↦ if(∪ (𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) → (𝑓‘𝑘) = ((𝑚 ∈ 𝐴 ↦ if(∪ (𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚)))‘𝑘))
151		fveq2 6645	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑘 → (𝐹‘𝑚) = (𝐹‘𝑘))
152	151	unieqd 4814	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑘 → ∪ (𝐹‘𝑚) = ∪ (𝐹‘𝑘))
153	152	breq1d 5040	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑘 → (∪ (𝐹‘𝑚) ≈ 1o ↔ ∪ (𝐹‘𝑘) ≈ 1o))
154	152	unieqd 4814	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑘 → ∪ ∪ (𝐹‘𝑚) = ∪ ∪ (𝐹‘𝑘))
155		fveq2 6645	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑘 → (𝑔‘𝑚) = (𝑔‘𝑘))
156	153, 154, 155	ifbieq12d 4452	. . . . . . . . . 10 ⊢ (𝑚 = 𝑘 → if(∪ (𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚)) = if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)))
157		fvex 6658	. . . . . . . . . . . . 13 ⊢ (𝐹‘𝑘) ∈ V
158	157	uniex 7447	. . . . . . . . . . . 12 ⊢ ∪ (𝐹‘𝑘) ∈ V
159	158	uniex 7447	. . . . . . . . . . 11 ⊢ ∪ ∪ (𝐹‘𝑘) ∈ V
160		fvex 6658	. . . . . . . . . . 11 ⊢ (𝑔‘𝑘) ∈ V
161	159, 160	ifex 4473	. . . . . . . . . 10 ⊢ if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ V
162	156, 118, 161	fvmpt 6745	. . . . . . . . 9 ⊢ (𝑘 ∈ 𝐴 → ((𝑚 ∈ 𝐴 ↦ if(∪ (𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚)))‘𝑘) = if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)))
163	150, 162	sylan9eq 2853	. . . . . . . 8 ⊢ ((𝑓 = (𝑚 ∈ 𝐴 ↦ if(∪ (𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) ∧ 𝑘 ∈ 𝐴) → (𝑓‘𝑘) = if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)))
164	163	eleq1d 2874	. . . . . . 7 ⊢ ((𝑓 = (𝑚 ∈ 𝐴 ↦ if(∪ (𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) ∧ 𝑘 ∈ 𝐴) → ((𝑓‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾) ↔ if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)))
165	164	ralbidva 3161	. . . . . 6 ⊢ (𝑓 = (𝑚 ∈ 𝐴 ↦ if(∪ (𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) → (∀𝑘 ∈ 𝐴 (𝑓‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾) ↔ ∀𝑘 ∈ 𝐴 if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)))
166	149, 165	anbi12d 633	. . . . 5 ⊢ (𝑓 = (𝑚 ∈ 𝐴 ↦ if(∪ (𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) → ((𝑓 Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (𝑓‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) ↔ ((𝑚 ∈ 𝐴 ↦ if(∪ (𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))))
167	166	spcegv 3545	. . . 4 ⊢ ((𝑚 ∈ 𝐴 ↦ if(∪ (𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) ∈ V → (((𝑚 ∈ 𝐴 ↦ if(∪ (𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (𝑓‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))))
168	167	3impib 1113	. . 3 ⊢ (((𝑚 ∈ 𝐴 ↦ if(∪ (𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) ∈ V ∧ (𝑚 ∈ 𝐴 ↦ if(∪ (𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (𝑓‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)))
169	111, 120, 148, 168	syl3anc 1368	. 2 ⊢ ((𝜑 ∧ (𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}⟶V ∧ ∀𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o} (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))) → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (𝑓‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)))
170	109, 169	exlimddv 1936	1 ⊢ (𝜑 → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (𝑓‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538  ∃wex 1781   ∈ wcel 2111  {cab 2776  ∀wral 3106  ∃wrex 3107  {crab 3110  Vcvv 3441   ∖ cdif 3878   ∩ cin 3880   ⊆ wss 3881  ∅c0 4243  ifcif 4425  𝒫 cpw 4497  {csn 4525  ∪ cuni 4800  ∪ ciun 4881   class class class wbr 5030   ↦ cmpt 5110  ^◡ccnv 5518  dom cdm 5519  ran crn 5520   “ cima 5522   Fn wfn 6319  ⟶wf 6320  ‘cfv 6324   ∈ cmpo 7137  1_oc1o 8078  Xcixp 8444   ≈ cen 8489  Fincfn 8492  cardccrd 9348  Compccmp 21991  UFLcufl 22505

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5154  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4801  df-int 4839  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5425  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-se 5479  df-we 5480  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-pred 6116  df-ord 6162  df-on 6163  df-lim 6164  df-suc 6165  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-isom 6333  df-riota 7093  df-ov 7138  df-oprab 7139  df-mpo 7140  df-om 7561  df-1st 7671  df-2nd 7672  df-wrecs 7930  df-recs 7991  df-rdg 8029  df-1o 8085  df-oadd 8089  df-omul 8090  df-er 8272  df-map 8391  df-ixp 8445  df-en 8493  df-dom 8494  df-fin 8496  df-wdom 9013  df-card 9352  df-acn 9355  df-cmp 21992

This theorem is referenced by:  ptcmplem4  22660