Theorem ptcmplem3 24388

Description: Lemma for ptcmp 24392. (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 5303	. . . 4 ⊢ (𝐴 ∈ 𝑉 → {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o} ∈ V)
3	1, 2	syl 18	. . 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 24387	. . . 4 ⊢ (𝜑 → ∪ 𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}∪ (𝐹‘𝑘) ∈ dom card)
12		eldifi 4070	. . . . . . . 8 ⊢ (𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾) → 𝑦 ∈ ∪ (𝐹‘𝑘))
13	12	3ad2ant3 1153	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ V ∧ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → 𝑦 ∈ ∪ (𝐹‘𝑘))
14	13	rabssdv 4002	. . . . . 6 ⊢ (𝜑 → {𝑦 ∈ V ∣ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)} ⊆ ∪ (𝐹‘𝑘))
15	14	ralrimivw 3162	. . . . 5 ⊢ (𝜑 → ∀𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o} {𝑦 ∈ V ∣ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)} ⊆ ∪ (𝐹‘𝑘))
16		ss2iun 4973	. . . . 5 ⊢ (∀𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o} {𝑦 ∈ V ∣ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)} ⊆ ∪ (𝐹‘𝑘) → ∪ 𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o} {𝑦 ∈ V ∣ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)} ⊆ ∪ 𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}∪ (𝐹‘𝑘))
17	15, 16	syl 18	. . . 4 ⊢ (𝜑 → ∪ 𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o} {𝑦 ∈ V ∣ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)} ⊆ ∪ 𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}∪ (𝐹‘𝑘))
18		ssnum 10131	. . . 4 ⊢ ((∪ 𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}∪ (𝐹‘𝑘) ∈ dom card ∧ ∪ 𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o} {𝑦 ∈ V ∣ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)} ⊆ ∪ 𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}∪ (𝐹‘𝑘)) → ∪ 𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o} {𝑦 ∈ V ∣ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)} ∈ dom card)
19	11, 17, 18	syl2anc 596	. . 3 ⊢ (𝜑 → ∪ 𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o} {𝑦 ∈ V ∣ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)} ∈ dom card)
20		elrabi 3644	. . . . 5 ⊢ (𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o} → 𝑘 ∈ 𝐴)
21	10	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ¬ ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = ∪ 𝑧)
22		ssdif0 4317	. . . . . . . . 9 ⊢ (∪ (𝐹‘𝑘) ⊆ ∪ 𝐾 ↔ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾) = ∅)
23	6	ffvelcdmda 7095	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐹‘𝑘) ∈ Comp)
24	23	adantr 486	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) → (𝐹‘𝑘) ∈ Comp)
25		ptcmplem3.8	. . . . . . . . . . . . . 14 ⊢ 𝐾 = {𝑢 ∈ (𝐹‘𝑘) ∣ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) ∈ 𝑈}
26	25	ssrab3 4010	. . . . . . . . . . . . 13 ⊢ 𝐾 ⊆ (𝐹‘𝑘)
27	26	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) → 𝐾 ⊆ (𝐹‘𝑘))
28		simpr 490	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) → ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾)
29		uniss 4878	. . . . . . . . . . . . . 14 ⊢ (𝐾 ⊆ (𝐹‘𝑘) → ∪ 𝐾 ⊆ ∪ (𝐹‘𝑘))
30	26, 29	mp1i 14	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) → ∪ 𝐾 ⊆ ∪ (𝐹‘𝑘))
31	28, 30	eqssd 3930	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) → ∪ (𝐹‘𝑘) = ∪ 𝐾)
32		eqid 2763	. . . . . . . . . . . . 13 ⊢ ∪ (𝐹‘𝑘) = ∪ (𝐹‘𝑘)
33	32	cmpcov 23722	. . . . . . . . . . . 12 ⊢ (((𝐹‘𝑘) ∈ Comp ∧ 𝐾 ⊆ (𝐹‘𝑘) ∧ ∪ (𝐹‘𝑘) = ∪ 𝐾) → ∃𝑡 ∈ (𝒫 𝐾 ∩ Fin)∪ (𝐹‘𝑘) = ∪ 𝑡)
34	24, 27, 31, 33	syl3anc 1398	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) → ∃𝑡 ∈ (𝒫 𝐾 ∩ Fin)∪ (𝐹‘𝑘) = ∪ 𝑡)
35		elfpw 9357	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ↔ (𝑡 ⊆ 𝐾 ∧ 𝑡 ∈ Fin))
36	35	simplbi 502	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) → 𝑡 ⊆ 𝐾)
37	36	ad2antrl 741	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → 𝑡 ⊆ 𝐾)
38	37	sselda 3913	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑥 ∈ 𝑡) → 𝑥 ∈ 𝐾)
39		imaeq2 6054	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢 = 𝑥 → (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) = (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥))
40	39	eleq1d 2849	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑢 = 𝑥 → ((◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) ∈ 𝑈 ↔ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) ∈ 𝑈))
41	40, 25	elrab2 3652	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ 𝐾 ↔ (𝑥 ∈ (𝐹‘𝑘) ∧ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) ∈ 𝑈))
42	41	simprbi 503	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ 𝐾 → (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) ∈ 𝑈)
43	38, 42	syl 18	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑥 ∈ 𝑡) → (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) ∈ 𝑈)
44	43	fmpttd 7126	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)):𝑡⟶𝑈)
45	44	frnd 6729	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) ⊆ 𝑈)
46	35	simprbi 503	. . . . . . . . . . . . . . 15 ⊢ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) → 𝑡 ∈ Fin)
47	46	ad2antrl 741	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → 𝑡 ∈ Fin)
48		eqid 2763	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) = (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥))
49	48	rnmpt 5944	. . . . . . . . . . . . . . 15 ⊢ ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) = {𝑓 ∣ ∃𝑥 ∈ 𝑡 𝑓 = (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)}
50		abrexfi 9355	. . . . . . . . . . . . . . 15 ⊢ (𝑡 ∈ Fin → {𝑓 ∣ ∃𝑥 ∈ 𝑡 𝑓 = (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)} ∈ Fin)
51	49, 50	eqeltrid 2868	. . . . . . . . . . . . . 14 ⊢ (𝑡 ∈ Fin → ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) ∈ Fin)
52	47, 51	syl 18	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) ∈ Fin)
53		elfpw 9357	. . . . . . . . . . . . 13 ⊢ (ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) ∈ (𝒫 𝑈 ∩ Fin) ↔ (ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) ⊆ 𝑈 ∧ ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) ∈ Fin))
54	45, 52, 53	sylanbrc 595	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) ∈ (𝒫 𝑈 ∩ Fin))
55		fveq2 6896	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = 𝑘 → (𝑓‘𝑛) = (𝑓‘𝑘))
56		fveq2 6896	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = 𝑘 → (𝐹‘𝑛) = (𝐹‘𝑘))
57	56	unieqd 4883	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = 𝑘 → ∪ (𝐹‘𝑛) = ∪ (𝐹‘𝑘))
58	55, 57	eleq12d 2858	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝑘 → ((𝑓‘𝑛) ∈ ∪ (𝐹‘𝑛) ↔ (𝑓‘𝑘) ∈ ∪ (𝐹‘𝑘)))
59		simpr 490	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑓 ∈ 𝑋) → 𝑓 ∈ 𝑋)
60	59, 5	eleqtrdi 2874	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑓 ∈ 𝑋) → 𝑓 ∈ X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛))
61		vex 3458	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 𝑓 ∈ V
62	61	elixp 8946	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓 ∈ X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛) ↔ (𝑓 Fn 𝐴 ∧ ∀𝑛 ∈ 𝐴 (𝑓‘𝑛) ∈ ∪ (𝐹‘𝑛)))
63	62	simprbi 503	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓 ∈ X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛) → ∀𝑛 ∈ 𝐴 (𝑓‘𝑛) ∈ ∪ (𝐹‘𝑛))
64	60, 63	syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑓 ∈ 𝑋) → ∀𝑛 ∈ 𝐴 (𝑓‘𝑛) ∈ ∪ (𝐹‘𝑛))
65		simp-4r 796	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑓 ∈ 𝑋) → 𝑘 ∈ 𝐴)
66	58, 64, 65	rspcdva 3581	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑓 ∈ 𝑋) → (𝑓‘𝑘) ∈ ∪ (𝐹‘𝑘))
67		simplrr 790	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑓 ∈ 𝑋) → ∪ (𝐹‘𝑘) = ∪ 𝑡)
68	66, 67	eleqtrd 2866	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑓 ∈ 𝑋) → (𝑓‘𝑘) ∈ ∪ 𝑡)
69		eluni2 4874	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓‘𝑘) ∈ ∪ 𝑡 ↔ ∃𝑥 ∈ 𝑡 (𝑓‘𝑘) ∈ 𝑥)
70	68, 69	sylib 221	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑓 ∈ 𝑋) → ∃𝑥 ∈ 𝑡 (𝑓‘𝑘) ∈ 𝑥)
71		fveq1 6895	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = 𝑓 → (𝑤‘𝑘) = (𝑓‘𝑘))
72	71	eleq1d 2849	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 = 𝑓 → ((𝑤‘𝑘) ∈ 𝑥 ↔ (𝑓‘𝑘) ∈ 𝑥))
73		eqid 2763	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) = (𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘))
74	73	mptpreima 6246	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) = {𝑤 ∈ 𝑋 ∣ (𝑤‘𝑘) ∈ 𝑥}
75	72, 74	elrab2 3652	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 ∈ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) ↔ (𝑓 ∈ 𝑋 ∧ (𝑓‘𝑘) ∈ 𝑥))
76	75	baib 545	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 ∈ 𝑋 → (𝑓 ∈ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) ↔ (𝑓‘𝑘) ∈ 𝑥))
77	76	ad2antlr 740	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑓 ∈ 𝑋) ∧ 𝑥 ∈ 𝑡) → (𝑓 ∈ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) ↔ (𝑓‘𝑘) ∈ 𝑥))
78	77	rexbidva 3188	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑓 ∈ 𝑋) → (∃𝑥 ∈ 𝑡 𝑓 ∈ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) ↔ ∃𝑥 ∈ 𝑡 (𝑓‘𝑘) ∈ 𝑥))
79	70, 78	mpbird 260	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑓 ∈ 𝑋) → ∃𝑥 ∈ 𝑡 𝑓 ∈ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥))
80		eliun 4958	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 ∈ ∪ 𝑥 ∈ 𝑡 (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) ↔ ∃𝑥 ∈ 𝑡 𝑓 ∈ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥))
81	79, 80	sylibr 237	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑓 ∈ 𝑋) → 𝑓 ∈ ∪ 𝑥 ∈ 𝑡 (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥))
82	81	ex 418	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → (𝑓 ∈ 𝑋 → 𝑓 ∈ ∪ 𝑥 ∈ 𝑡 (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)))
83	82	ssrdv 3919	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → 𝑋 ⊆ ∪ 𝑥 ∈ 𝑡 (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥))
84	43	ralrimiva 3158	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → ∀𝑥 ∈ 𝑡 (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) ∈ 𝑈)
85		dfiun2g 4991	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑥 ∈ 𝑡 (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) ∈ 𝑈 → ∪ 𝑥 ∈ 𝑡 (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) = ∪ {𝑓 ∣ ∃𝑥 ∈ 𝑡 𝑓 = (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)})
86	84, 85	syl 18	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → ∪ 𝑥 ∈ 𝑡 (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) = ∪ {𝑓 ∣ ∃𝑥 ∈ 𝑡 𝑓 = (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)})
87	49	unieqi 4882	. . . . . . . . . . . . . . 15 ⊢ ∪ ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) = ∪ {𝑓 ∣ ∃𝑥 ∈ 𝑡 𝑓 = (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)}
88	86, 87	eqtr4di 2816	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → ∪ 𝑥 ∈ 𝑡 (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) = ∪ ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)))
89	83, 88	sseqtrd 3949	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → 𝑋 ⊆ ∪ ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)))
90	45	unissd 4880	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → ∪ ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) ⊆ ∪ 𝑈)
91	9	ad3antrrr 743	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → 𝑋 = ∪ 𝑈)
92	90, 91	sseqtrrd 3950	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → ∪ ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) ⊆ 𝑋)
93	89, 92	eqssd 3930	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → 𝑋 = ∪ ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)))
94		unieq 4881	. . . . . . . . . . . . 13 ⊢ (𝑧 = ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) → ∪ 𝑧 = ∪ ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)))
95	94	rspceeqv 3602	. . . . . . . . . . . 12 ⊢ ((ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑋 = ∪ ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥))) → ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = ∪ 𝑧)
96	54, 93, 95	syl2anc 596	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = ∪ 𝑧)
97	34, 96	rexlimddv 3173	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) → ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = ∪ 𝑧)
98	97	ex 418	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (∪ (𝐹‘𝑘) ⊆ ∪ 𝐾 → ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = ∪ 𝑧))
99	22, 98	biimtrrid 246	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((∪ (𝐹‘𝑘) ∖ ∪ 𝐾) = ∅ → ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = ∪ 𝑧))
100	21, 99	mtod 201	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ¬ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾) = ∅)
101		neq0 4302	. . . . . . 7 ⊢ (¬ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾) = ∅ ↔ ∃𝑦 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))
102	100, 101	sylib 221	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ∃𝑦 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))
103		rexv 3481	. . . . . 6 ⊢ (∃𝑦 ∈ V 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾) ↔ ∃𝑦 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))
104	102, 103	sylibr 237	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ∃𝑦 ∈ V 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))
105	20, 104	sylan2 605	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}) → ∃𝑦 ∈ V 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))
106	105	ralrimiva 3158	. . 3 ⊢ (𝜑 → ∀𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}∃𝑦 ∈ V 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))
107		eleq1 2852	. . . 4 ⊢ (𝑦 = (𝑔‘𝑘) → (𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾) ↔ (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)))
108	107	ac6num 10570	. . 3 ⊢ (({𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o} ∈ V ∧ ∪ 𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o} {𝑦 ∈ V ∣ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)} ∈ dom card ∧ ∀𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}∃𝑦 ∈ V 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → ∃𝑔(𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}⟶V ∧ ∀𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o} (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)))
109	3, 19, 106, 108	syl3anc 1398	. 2 ⊢ (𝜑 → ∃𝑔(𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}⟶V ∧ ∀𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o} (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)))
110	1	adantr 486	. . . 4 ⊢ ((𝜑 ∧ (𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}⟶V ∧ ∀𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o} (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))) → 𝐴 ∈ 𝑉)
111	110	mptexd 7240	. . 3 ⊢ ((𝜑 ∧ (𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}⟶V ∧ ∀𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o} (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))) → (𝑚 ∈ 𝐴 ↦ if(∪ (𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) ∈ V)
112		fvex 6909	. . . . . . . 8 ⊢ (𝐹‘𝑚) ∈ V
113	112	uniex 7768	. . . . . . 7 ⊢ ∪ (𝐹‘𝑚) ∈ V
114	113	uniex 7768	. . . . . 6 ⊢ ∪ ∪ (𝐹‘𝑚) ∈ V
115		fvex 6909	. . . . . 6 ⊢ (𝑔‘𝑚) ∈ V
116	114, 115	ifex 4536	. . . . 5 ⊢ if(∪ (𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚)) ∈ V
117	116	rgenw 3084	. . . 4 ⊢ ∀𝑚 ∈ 𝐴 if(∪ (𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚)) ∈ V
118		eqid 2763	. . . . 5 ⊢ (𝑚 ∈ 𝐴 ↦ if(∪ (𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) = (𝑚 ∈ 𝐴 ↦ if(∪ (𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚)))
119	118	fnmpt 6690	. . . 4 ⊢ (∀𝑚 ∈ 𝐴 if(∪ (𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚)) ∈ V → (𝑚 ∈ 𝐴 ↦ if(∪ (𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) Fn 𝐴)
120	117, 119	mp1i 14	. . 3 ⊢ ((𝜑 ∧ (𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}⟶V ∧ ∀𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o} (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))) → (𝑚 ∈ 𝐴 ↦ if(∪ (𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) Fn 𝐴)
121	57	breq1d 5116	. . . . . . 7 ⊢ (𝑛 = 𝑘 → (∪ (𝐹‘𝑛) ≈ 1o ↔ ∪ (𝐹‘𝑘) ≈ 1o))
122	121	notbid 321	. . . . . 6 ⊢ (𝑛 = 𝑘 → (¬ ∪ (𝐹‘𝑛) ≈ 1o ↔ ¬ ∪ (𝐹‘𝑘) ≈ 1o))
123	122	ralrab 3655	. . . . 5 ⊢ (∀𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o} (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾) ↔ ∀𝑘 ∈ 𝐴 (¬ ∪ (𝐹‘𝑘) ≈ 1o → (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)))
124		iftrue 4491	. . . . . . . . . . 11 ⊢ (∪ (𝐹‘𝑘) ≈ 1o → if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) = ∪ ∪ (𝐹‘𝑘))
125	124	ad2antll 742	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}⟶V) ∧ (𝑘 ∈ 𝐴 ∧ ∪ (𝐹‘𝑘) ≈ 1o)) → if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) = ∪ ∪ (𝐹‘𝑘))
126	102	adantrr 730	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑘 ∈ 𝐴 ∧ ∪ (𝐹‘𝑘) ≈ 1o)) → ∃𝑦 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))
127	12	adantl 487	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑘 ∈ 𝐴 ∧ ∪ (𝐹‘𝑘) ≈ 1o)) ∧ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → 𝑦 ∈ ∪ (𝐹‘𝑘))
128		simplrr 790	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑘 ∈ 𝐴 ∧ ∪ (𝐹‘𝑘) ≈ 1o)) ∧ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → ∪ (𝐹‘𝑘) ≈ 1o)
129		en1b 9066	. . . . . . . . . . . . . . . 16 ⊢ (∪ (𝐹‘𝑘) ≈ 1o ↔ ∪ (𝐹‘𝑘) = {∪ ∪ (𝐹‘𝑘)})
130	128, 129	sylib 221	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑘 ∈ 𝐴 ∧ ∪ (𝐹‘𝑘) ≈ 1o)) ∧ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → ∪ (𝐹‘𝑘) = {∪ ∪ (𝐹‘𝑘)})
131	127, 130	eleqtrd 2866	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑘 ∈ 𝐴 ∧ ∪ (𝐹‘𝑘) ≈ 1o)) ∧ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → 𝑦 ∈ {∪ ∪ (𝐹‘𝑘)})
132		elsni 4601	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ {∪ ∪ (𝐹‘𝑘)} → 𝑦 = ∪ ∪ (𝐹‘𝑘))
133	131, 132	syl 18	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑘 ∈ 𝐴 ∧ ∪ (𝐹‘𝑘) ≈ 1o)) ∧ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → 𝑦 = ∪ ∪ (𝐹‘𝑘))
134		simpr 490	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑘 ∈ 𝐴 ∧ ∪ (𝐹‘𝑘) ≈ 1o)) ∧ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))
135	133, 134	eqeltrrd 2865	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑘 ∈ 𝐴 ∧ ∪ (𝐹‘𝑘) ≈ 1o)) ∧ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → ∪ ∪ (𝐹‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))
136	126, 135	exlimddv 1969	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑘 ∈ 𝐴 ∧ ∪ (𝐹‘𝑘) ≈ 1o)) → ∪ ∪ (𝐹‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))
137	136	adantlr 728	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}⟶V) ∧ (𝑘 ∈ 𝐴 ∧ ∪ (𝐹‘𝑘) ≈ 1o)) → ∪ ∪ (𝐹‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))
138	125, 137	eqeltrd 2864	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}⟶V) ∧ (𝑘 ∈ 𝐴 ∧ ∪ (𝐹‘𝑘) ≈ 1o)) → if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))
139	138	a1d 26	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}⟶V) ∧ (𝑘 ∈ 𝐴 ∧ ∪ (𝐹‘𝑘) ≈ 1o)) → ((¬ ∪ (𝐹‘𝑘) ≈ 1o → (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)))
140	139	expr 462	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}⟶V) ∧ 𝑘 ∈ 𝐴) → (∪ (𝐹‘𝑘) ≈ 1o → ((¬ ∪ (𝐹‘𝑘) ≈ 1o → (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))))
141		pm2.27 43	. . . . . . . 8 ⊢ (¬ ∪ (𝐹‘𝑘) ≈ 1o → ((¬ ∪ (𝐹‘𝑘) ≈ 1o → (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)))
142		iffalse 4494	. . . . . . . . 9 ⊢ (¬ ∪ (𝐹‘𝑘) ≈ 1o → if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) = (𝑔‘𝑘))
143	142	eleq1d 2849	. . . . . . . 8 ⊢ (¬ ∪ (𝐹‘𝑘) ≈ 1o → (if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾) ↔ (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)))
144	141, 143	sylibrd 262	. . . . . . 7 ⊢ (¬ ∪ (𝐹‘𝑘) ≈ 1o → ((¬ ∪ (𝐹‘𝑘) ≈ 1o → (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)))
145	140, 144	pm2.61d1 182	. . . . . 6 ⊢ (((𝜑 ∧ 𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}⟶V) ∧ 𝑘 ∈ 𝐴) → ((¬ ∪ (𝐹‘𝑘) ≈ 1o → (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)))
146	145	ralimdva 3178	. . . . 5 ⊢ ((𝜑 ∧ 𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}⟶V) → (∀𝑘 ∈ 𝐴 (¬ ∪ (𝐹‘𝑘) ≈ 1o → (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → ∀𝑘 ∈ 𝐴 if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)))
147	123, 146	biimtrid 245	. . . 4 ⊢ ((𝜑 ∧ 𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}⟶V) → (∀𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o} (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾) → ∀𝑘 ∈ 𝐴 if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)))
148	147	impr 460	. . 3 ⊢ ((𝜑 ∧ (𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}⟶V ∧ ∀𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o} (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))) → ∀𝑘 ∈ 𝐴 if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))
149		fneq1 6641	. . . . . 6 ⊢ (𝑓 = (𝑚 ∈ 𝐴 ↦ if(∪ (𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) → (𝑓 Fn 𝐴 ↔ (𝑚 ∈ 𝐴 ↦ if(∪ (𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) Fn 𝐴))
150		fveq1 6895	. . . . . . . . 9 ⊢ (𝑓 = (𝑚 ∈ 𝐴 ↦ if(∪ (𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) → (𝑓‘𝑘) = ((𝑚 ∈ 𝐴 ↦ if(∪ (𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚)))‘𝑘))
151		fveq2 6896	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑘 → (𝐹‘𝑚) = (𝐹‘𝑘))
152	151	unieqd 4883	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑘 → ∪ (𝐹‘𝑚) = ∪ (𝐹‘𝑘))
153	152	breq1d 5116	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑘 → (∪ (𝐹‘𝑚) ≈ 1o ↔ ∪ (𝐹‘𝑘) ≈ 1o))
154	152	unieqd 4883	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑘 → ∪ ∪ (𝐹‘𝑚) = ∪ ∪ (𝐹‘𝑘))
155		fveq2 6896	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑘 → (𝑔‘𝑚) = (𝑔‘𝑘))
156	153, 154, 155	ifbieq12d 4514	. . . . . . . . . 10 ⊢ (𝑚 = 𝑘 → if(∪ (𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚)) = if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)))
157		fvex 6909	. . . . . . . . . . . . 13 ⊢ (𝐹‘𝑘) ∈ V
158	157	uniex 7768	. . . . . . . . . . . 12 ⊢ ∪ (𝐹‘𝑘) ∈ V
159	158	uniex 7768	. . . . . . . . . . 11 ⊢ ∪ ∪ (𝐹‘𝑘) ∈ V
160		fvex 6909	. . . . . . . . . . 11 ⊢ (𝑔‘𝑘) ∈ V
161	159, 160	ifex 4536	. . . . . . . . . 10 ⊢ if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ V
162	156, 118, 161	fvmpt 7004	. . . . . . . . 9 ⊢ (𝑘 ∈ 𝐴 → ((𝑚 ∈ 𝐴 ↦ if(∪ (𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚)))‘𝑘) = if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)))
163	150, 162	sylan9eq 2818	. . . . . . . 8 ⊢ ((𝑓 = (𝑚 ∈ 𝐴 ↦ if(∪ (𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) ∧ 𝑘 ∈ 𝐴) → (𝑓‘𝑘) = if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)))
164	163	eleq1d 2849	. . . . . . 7 ⊢ ((𝑓 = (𝑚 ∈ 𝐴 ↦ if(∪ (𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) ∧ 𝑘 ∈ 𝐴) → ((𝑓‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾) ↔ if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)))
165	164	ralbidva 3187	. . . . . 6 ⊢ (𝑓 = (𝑚 ∈ 𝐴 ↦ if(∪ (𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) → (∀𝑘 ∈ 𝐴 (𝑓‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾) ↔ ∀𝑘 ∈ 𝐴 if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)))
166	149, 165	anbi12d 644	. . . . 5 ⊢ (𝑓 = (𝑚 ∈ 𝐴 ↦ if(∪ (𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) → ((𝑓 Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (𝑓‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) ↔ ((𝑚 ∈ 𝐴 ↦ if(∪ (𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))))
167	166	spcegv 3555	. . . 4 ⊢ ((𝑚 ∈ 𝐴 ↦ if(∪ (𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) ∈ V → (((𝑚 ∈ 𝐴 ↦ if(∪ (𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (𝑓‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))))
168	167	3impib 1134	. . 3 ⊢ (((𝑚 ∈ 𝐴 ↦ if(∪ (𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) ∈ V ∧ (𝑚 ∈ 𝐴 ↦ if(∪ (𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (𝑓‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)))
169	111, 120, 148, 168	syl3anc 1398	. 2 ⊢ ((𝜑 ∧ (𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}⟶V ∧ ∀𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o} (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))) → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (𝑓‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)))
170	109, 169	exlimddv 1969	1 ⊢ (𝜑 → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (𝑓‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1569  ∃wex 1811   ∈ wcel 2146  {cab 2741  ∀wral 3080  ∃wrex 3090  {crab 3416  Vcvv 3454   ⊆ wss 3900   ∖ cdif 4048   ∩ cin 4092  ∅c0 4281  ifcif 4485  𝒫 cpw 4560  {csn 4588  ∪ cuni 4870  ∪ ciun 4954   class class class wbr 5106   ↦ cmpt 5189  ^◡ccnv 5654  dom cdm 5655  ran crn 5656   “ cima 5658   Fn wfn 6542  ⟶wf 6543  ‘cfv 6547   ∈ cmpo 7432  1_oc1o 8483  Xcixp 8939   ≈ cen 8984  Fincfn 8987  cardccrd 10029  Compccmp 23719  UFLcufl 24234

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2196  ax-12 2215  ax-ext 2735  ax-rep 5235  ax-sep 5252  ax-nul 5263  ax-pow 5331  ax-pr 5395  ax-un 7761

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2101  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-int 4911  df-iun 4956  df-br 5107  df-opab 5171  df-mpt 5190  df-tr 5216  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-se 5609  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6311  df-ord 6372  df-on 6373  df-lim 6374  df-suc 6375  df-iota 6501  df-fun 6549  df-fn 6550  df-f 6551  df-f1 6552  df-fo 6553  df-f1o 6554  df-fv 6555  df-isom 6556  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-om 7888  df-1st 8011  df-2nd 8012  df-frecs 8313  df-wrecs 8344  df-recs 8393  df-rdg 8432  df-1o 8490  df-oadd 8494  df-omul 8495  df-er 8731  df-map 8863  df-ixp 8940  df-en 8988  df-dom 8989  df-fin 8991  df-wdom 9572  df-card 10033  df-acn 10036  df-cmp 23720

This theorem is used by:  ptcmplem4  24389