Theorem ptcmplem3 24062

Description: Lemma for ptcmp 24066. (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 5337	. . . 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 24061	. . . 4 ⊢ (𝜑 → ∪ 𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}∪ (𝐹‘𝑘) ∈ dom card)
12		eldifi 4131	. . . . . . . 8 ⊢ (𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾) → 𝑦 ∈ ∪ (𝐹‘𝑘))
13	12	3ad2ant3 1136	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ V ∧ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → 𝑦 ∈ ∪ (𝐹‘𝑘))
14	13	rabssdv 4075	. . . . . 6 ⊢ (𝜑 → {𝑦 ∈ V ∣ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)} ⊆ ∪ (𝐹‘𝑘))
15	14	ralrimivw 3150	. . . . 5 ⊢ (𝜑 → ∀𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o} {𝑦 ∈ V ∣ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)} ⊆ ∪ (𝐹‘𝑘))
16		ss2iun 5010	. . . . 5 ⊢ (∀𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o} {𝑦 ∈ V ∣ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)} ⊆ ∪ (𝐹‘𝑘) → ∪ 𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o} {𝑦 ∈ V ∣ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)} ⊆ ∪ 𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}∪ (𝐹‘𝑘))
17	15, 16	syl 17	. . . 4 ⊢ (𝜑 → ∪ 𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o} {𝑦 ∈ V ∣ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)} ⊆ ∪ 𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}∪ (𝐹‘𝑘))
18		ssnum 10079	. . . 4 ⊢ ((∪ 𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}∪ (𝐹‘𝑘) ∈ dom card ∧ ∪ 𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o} {𝑦 ∈ V ∣ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)} ⊆ ∪ 𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}∪ (𝐹‘𝑘)) → ∪ 𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o} {𝑦 ∈ V ∣ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)} ∈ dom card)
19	11, 17, 18	syl2anc 584	. . 3 ⊢ (𝜑 → ∪ 𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o} {𝑦 ∈ V ∣ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)} ∈ dom card)
20		elrabi 3687	. . . . 5 ⊢ (𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o} → 𝑘 ∈ 𝐴)
21	10	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ¬ ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = ∪ 𝑧)
22		ssdif0 4366	. . . . . . . . 9 ⊢ (∪ (𝐹‘𝑘) ⊆ ∪ 𝐾 ↔ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾) = ∅)
23	6	ffvelcdmda 7104	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐹‘𝑘) ∈ Comp)
24	23	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) → (𝐹‘𝑘) ∈ Comp)
25		ptcmplem3.8	. . . . . . . . . . . . . 14 ⊢ 𝐾 = {𝑢 ∈ (𝐹‘𝑘) ∣ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) ∈ 𝑈}
26	25	ssrab3 4082	. . . . . . . . . . . . 13 ⊢ 𝐾 ⊆ (𝐹‘𝑘)
27	26	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) → 𝐾 ⊆ (𝐹‘𝑘))
28		simpr 484	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) → ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾)
29		uniss 4915	. . . . . . . . . . . . . 14 ⊢ (𝐾 ⊆ (𝐹‘𝑘) → ∪ 𝐾 ⊆ ∪ (𝐹‘𝑘))
30	26, 29	mp1i 13	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) → ∪ 𝐾 ⊆ ∪ (𝐹‘𝑘))
31	28, 30	eqssd 4001	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) → ∪ (𝐹‘𝑘) = ∪ 𝐾)
32		eqid 2737	. . . . . . . . . . . . 13 ⊢ ∪ (𝐹‘𝑘) = ∪ (𝐹‘𝑘)
33	32	cmpcov 23397	. . . . . . . . . . . 12 ⊢ (((𝐹‘𝑘) ∈ Comp ∧ 𝐾 ⊆ (𝐹‘𝑘) ∧ ∪ (𝐹‘𝑘) = ∪ 𝐾) → ∃𝑡 ∈ (𝒫 𝐾 ∩ Fin)∪ (𝐹‘𝑘) = ∪ 𝑡)
34	24, 27, 31, 33	syl3anc 1373	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) → ∃𝑡 ∈ (𝒫 𝐾 ∩ Fin)∪ (𝐹‘𝑘) = ∪ 𝑡)
35		elfpw 9394	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ↔ (𝑡 ⊆ 𝐾 ∧ 𝑡 ∈ Fin))
36	35	simplbi 497	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) → 𝑡 ⊆ 𝐾)
37	36	ad2antrl 728	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → 𝑡 ⊆ 𝐾)
38	37	sselda 3983	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑥 ∈ 𝑡) → 𝑥 ∈ 𝐾)
39		imaeq2 6074	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢 = 𝑥 → (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) = (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥))
40	39	eleq1d 2826	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑢 = 𝑥 → ((◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) ∈ 𝑈 ↔ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) ∈ 𝑈))
41	40, 25	elrab2 3695	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ 𝐾 ↔ (𝑥 ∈ (𝐹‘𝑘) ∧ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) ∈ 𝑈))
42	41	simprbi 496	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ 𝐾 → (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) ∈ 𝑈)
43	38, 42	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑥 ∈ 𝑡) → (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) ∈ 𝑈)
44	43	fmpttd 7135	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)):𝑡⟶𝑈)
45	44	frnd 6744	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) ⊆ 𝑈)
46	35	simprbi 496	. . . . . . . . . . . . . . 15 ⊢ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) → 𝑡 ∈ Fin)
47	46	ad2antrl 728	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → 𝑡 ∈ Fin)
48		eqid 2737	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) = (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥))
49	48	rnmpt 5968	. . . . . . . . . . . . . . 15 ⊢ ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) = {𝑓 ∣ ∃𝑥 ∈ 𝑡 𝑓 = (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)}
50		abrexfi 9392	. . . . . . . . . . . . . . 15 ⊢ (𝑡 ∈ Fin → {𝑓 ∣ ∃𝑥 ∈ 𝑡 𝑓 = (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)} ∈ Fin)
51	49, 50	eqeltrid 2845	. . . . . . . . . . . . . 14 ⊢ (𝑡 ∈ Fin → ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) ∈ Fin)
52	47, 51	syl 17	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) ∈ Fin)
53		elfpw 9394	. . . . . . . . . . . . 13 ⊢ (ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) ∈ (𝒫 𝑈 ∩ Fin) ↔ (ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) ⊆ 𝑈 ∧ ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) ∈ Fin))
54	45, 52, 53	sylanbrc 583	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) ∈ (𝒫 𝑈 ∩ Fin))
55		fveq2 6906	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = 𝑘 → (𝑓‘𝑛) = (𝑓‘𝑘))
56		fveq2 6906	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = 𝑘 → (𝐹‘𝑛) = (𝐹‘𝑘))
57	56	unieqd 4920	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 = 𝑘 → ∪ (𝐹‘𝑛) = ∪ (𝐹‘𝑘))
58	55, 57	eleq12d 2835	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝑘 → ((𝑓‘𝑛) ∈ ∪ (𝐹‘𝑛) ↔ (𝑓‘𝑘) ∈ ∪ (𝐹‘𝑘)))
59		simpr 484	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑓 ∈ 𝑋) → 𝑓 ∈ 𝑋)
60	59, 5	eleqtrdi 2851	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑓 ∈ 𝑋) → 𝑓 ∈ X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛))
61		vex 3484	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 𝑓 ∈ V
62	61	elixp 8944	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓 ∈ X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛) ↔ (𝑓 Fn 𝐴 ∧ ∀𝑛 ∈ 𝐴 (𝑓‘𝑛) ∈ ∪ (𝐹‘𝑛)))
63	62	simprbi 496	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓 ∈ X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛) → ∀𝑛 ∈ 𝐴 (𝑓‘𝑛) ∈ ∪ (𝐹‘𝑛))
64	60, 63	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑓 ∈ 𝑋) → ∀𝑛 ∈ 𝐴 (𝑓‘𝑛) ∈ ∪ (𝐹‘𝑛))
65		simp-4r 784	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑓 ∈ 𝑋) → 𝑘 ∈ 𝐴)
66	58, 64, 65	rspcdva 3623	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑓 ∈ 𝑋) → (𝑓‘𝑘) ∈ ∪ (𝐹‘𝑘))
67		simplrr 778	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑓 ∈ 𝑋) → ∪ (𝐹‘𝑘) = ∪ 𝑡)
68	66, 67	eleqtrd 2843	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑓 ∈ 𝑋) → (𝑓‘𝑘) ∈ ∪ 𝑡)
69		eluni2 4911	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓‘𝑘) ∈ ∪ 𝑡 ↔ ∃𝑥 ∈ 𝑡 (𝑓‘𝑘) ∈ 𝑥)
70	68, 69	sylib 218	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑓 ∈ 𝑋) → ∃𝑥 ∈ 𝑡 (𝑓‘𝑘) ∈ 𝑥)
71		fveq1 6905	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = 𝑓 → (𝑤‘𝑘) = (𝑓‘𝑘))
72	71	eleq1d 2826	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 = 𝑓 → ((𝑤‘𝑘) ∈ 𝑥 ↔ (𝑓‘𝑘) ∈ 𝑥))
73		eqid 2737	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) = (𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘))
74	73	mptpreima 6258	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) = {𝑤 ∈ 𝑋 ∣ (𝑤‘𝑘) ∈ 𝑥}
75	72, 74	elrab2 3695	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 ∈ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) ↔ (𝑓 ∈ 𝑋 ∧ (𝑓‘𝑘) ∈ 𝑥))
76	75	baib 535	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 ∈ 𝑋 → (𝑓 ∈ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) ↔ (𝑓‘𝑘) ∈ 𝑥))
77	76	ad2antlr 727	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑓 ∈ 𝑋) ∧ 𝑥 ∈ 𝑡) → (𝑓 ∈ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) ↔ (𝑓‘𝑘) ∈ 𝑥))
78	77	rexbidva 3177	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑓 ∈ 𝑋) → (∃𝑥 ∈ 𝑡 𝑓 ∈ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) ↔ ∃𝑥 ∈ 𝑡 (𝑓‘𝑘) ∈ 𝑥))
79	70, 78	mpbird 257	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑓 ∈ 𝑋) → ∃𝑥 ∈ 𝑡 𝑓 ∈ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥))
80		eliun 4995	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 ∈ ∪ 𝑥 ∈ 𝑡 (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) ↔ ∃𝑥 ∈ 𝑡 𝑓 ∈ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥))
81	79, 80	sylibr 234	. . . . . . . . . . . . . . . 16 ⊢ (((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) ∧ 𝑓 ∈ 𝑋) → 𝑓 ∈ ∪ 𝑥 ∈ 𝑡 (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥))
82	81	ex 412	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → (𝑓 ∈ 𝑋 → 𝑓 ∈ ∪ 𝑥 ∈ 𝑡 (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)))
83	82	ssrdv 3989	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → 𝑋 ⊆ ∪ 𝑥 ∈ 𝑡 (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥))
84	43	ralrimiva 3146	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → ∀𝑥 ∈ 𝑡 (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) ∈ 𝑈)
85		dfiun2g 5030	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑥 ∈ 𝑡 (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) ∈ 𝑈 → ∪ 𝑥 ∈ 𝑡 (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) = ∪ {𝑓 ∣ ∃𝑥 ∈ 𝑡 𝑓 = (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)})
86	84, 85	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → ∪ 𝑥 ∈ 𝑡 (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) = ∪ {𝑓 ∣ ∃𝑥 ∈ 𝑡 𝑓 = (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)})
87	49	unieqi 4919	. . . . . . . . . . . . . . 15 ⊢ ∪ ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) = ∪ {𝑓 ∣ ∃𝑥 ∈ 𝑡 𝑓 = (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)}
88	86, 87	eqtr4di 2795	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → ∪ 𝑥 ∈ 𝑡 (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥) = ∪ ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)))
89	83, 88	sseqtrd 4020	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → 𝑋 ⊆ ∪ ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)))
90	45	unissd 4917	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → ∪ ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) ⊆ ∪ 𝑈)
91	9	ad3antrrr 730	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → 𝑋 = ∪ 𝑈)
92	90, 91	sseqtrrd 4021	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → ∪ ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) ⊆ 𝑋)
93	89, 92	eqssd 4001	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → 𝑋 = ∪ ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)))
94		unieq 4918	. . . . . . . . . . . . 13 ⊢ (𝑧 = ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) → ∪ 𝑧 = ∪ ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)))
95	94	rspceeqv 3645	. . . . . . . . . . . 12 ⊢ ((ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥)) ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑋 = ∪ ran (𝑥 ∈ 𝑡 ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑥))) → ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = ∪ 𝑧)
96	54, 93, 95	syl2anc 584	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ ∪ (𝐹‘𝑘) = ∪ 𝑡)) → ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = ∪ 𝑧)
97	34, 96	rexlimddv 3161	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ 𝐴) ∧ ∪ (𝐹‘𝑘) ⊆ ∪ 𝐾) → ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = ∪ 𝑧)
98	97	ex 412	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (∪ (𝐹‘𝑘) ⊆ ∪ 𝐾 → ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = ∪ 𝑧))
99	22, 98	biimtrrid 243	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ((∪ (𝐹‘𝑘) ∖ ∪ 𝐾) = ∅ → ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = ∪ 𝑧))
100	21, 99	mtod 198	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ¬ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾) = ∅)
101		neq0 4352	. . . . . . 7 ⊢ (¬ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾) = ∅ ↔ ∃𝑦 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))
102	100, 101	sylib 218	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ∃𝑦 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))
103		rexv 3509	. . . . . 6 ⊢ (∃𝑦 ∈ V 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾) ↔ ∃𝑦 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))
104	102, 103	sylibr 234	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → ∃𝑦 ∈ V 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))
105	20, 104	sylan2 593	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}) → ∃𝑦 ∈ V 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))
106	105	ralrimiva 3146	. . 3 ⊢ (𝜑 → ∀𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}∃𝑦 ∈ V 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))
107		eleq1 2829	. . . 4 ⊢ (𝑦 = (𝑔‘𝑘) → (𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾) ↔ (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)))
108	107	ac6num 10519	. . 3 ⊢ (({𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o} ∈ V ∧ ∪ 𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o} {𝑦 ∈ V ∣ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)} ∈ dom card ∧ ∀𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}∃𝑦 ∈ V 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → ∃𝑔(𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}⟶V ∧ ∀𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o} (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)))
109	3, 19, 106, 108	syl3anc 1373	. 2 ⊢ (𝜑 → ∃𝑔(𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}⟶V ∧ ∀𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o} (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)))
110	1	adantr 480	. . . 4 ⊢ ((𝜑 ∧ (𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}⟶V ∧ ∀𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o} (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))) → 𝐴 ∈ 𝑉)
111	110	mptexd 7244	. . 3 ⊢ ((𝜑 ∧ (𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}⟶V ∧ ∀𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o} (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))) → (𝑚 ∈ 𝐴 ↦ if(∪ (𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) ∈ V)
112		fvex 6919	. . . . . . . 8 ⊢ (𝐹‘𝑚) ∈ V
113	112	uniex 7761	. . . . . . 7 ⊢ ∪ (𝐹‘𝑚) ∈ V
114	113	uniex 7761	. . . . . 6 ⊢ ∪ ∪ (𝐹‘𝑚) ∈ V
115		fvex 6919	. . . . . 6 ⊢ (𝑔‘𝑚) ∈ V
116	114, 115	ifex 4576	. . . . 5 ⊢ if(∪ (𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚)) ∈ V
117	116	rgenw 3065	. . . 4 ⊢ ∀𝑚 ∈ 𝐴 if(∪ (𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚)) ∈ V
118		eqid 2737	. . . . 5 ⊢ (𝑚 ∈ 𝐴 ↦ if(∪ (𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) = (𝑚 ∈ 𝐴 ↦ if(∪ (𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚)))
119	118	fnmpt 6708	. . . 4 ⊢ (∀𝑚 ∈ 𝐴 if(∪ (𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚)) ∈ V → (𝑚 ∈ 𝐴 ↦ if(∪ (𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) Fn 𝐴)
120	117, 119	mp1i 13	. . 3 ⊢ ((𝜑 ∧ (𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}⟶V ∧ ∀𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o} (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))) → (𝑚 ∈ 𝐴 ↦ if(∪ (𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) Fn 𝐴)
121	57	breq1d 5153	. . . . . . 7 ⊢ (𝑛 = 𝑘 → (∪ (𝐹‘𝑛) ≈ 1o ↔ ∪ (𝐹‘𝑘) ≈ 1o))
122	121	notbid 318	. . . . . 6 ⊢ (𝑛 = 𝑘 → (¬ ∪ (𝐹‘𝑛) ≈ 1o ↔ ¬ ∪ (𝐹‘𝑘) ≈ 1o))
123	122	ralrab 3699	. . . . 5 ⊢ (∀𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o} (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾) ↔ ∀𝑘 ∈ 𝐴 (¬ ∪ (𝐹‘𝑘) ≈ 1o → (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)))
124		iftrue 4531	. . . . . . . . . . 11 ⊢ (∪ (𝐹‘𝑘) ≈ 1o → if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) = ∪ ∪ (𝐹‘𝑘))
125	124	ad2antll 729	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}⟶V) ∧ (𝑘 ∈ 𝐴 ∧ ∪ (𝐹‘𝑘) ≈ 1o)) → if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) = ∪ ∪ (𝐹‘𝑘))
126	102	adantrr 717	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑘 ∈ 𝐴 ∧ ∪ (𝐹‘𝑘) ≈ 1o)) → ∃𝑦 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))
127	12	adantl 481	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑘 ∈ 𝐴 ∧ ∪ (𝐹‘𝑘) ≈ 1o)) ∧ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → 𝑦 ∈ ∪ (𝐹‘𝑘))
128		simplrr 778	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑘 ∈ 𝐴 ∧ ∪ (𝐹‘𝑘) ≈ 1o)) ∧ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → ∪ (𝐹‘𝑘) ≈ 1o)
129		en1b 9065	. . . . . . . . . . . . . . . 16 ⊢ (∪ (𝐹‘𝑘) ≈ 1o ↔ ∪ (𝐹‘𝑘) = {∪ ∪ (𝐹‘𝑘)})
130	128, 129	sylib 218	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑘 ∈ 𝐴 ∧ ∪ (𝐹‘𝑘) ≈ 1o)) ∧ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → ∪ (𝐹‘𝑘) = {∪ ∪ (𝐹‘𝑘)})
131	127, 130	eleqtrd 2843	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑘 ∈ 𝐴 ∧ ∪ (𝐹‘𝑘) ≈ 1o)) ∧ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → 𝑦 ∈ {∪ ∪ (𝐹‘𝑘)})
132		elsni 4643	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ {∪ ∪ (𝐹‘𝑘)} → 𝑦 = ∪ ∪ (𝐹‘𝑘))
133	131, 132	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑘 ∈ 𝐴 ∧ ∪ (𝐹‘𝑘) ≈ 1o)) ∧ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → 𝑦 = ∪ ∪ (𝐹‘𝑘))
134		simpr 484	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑘 ∈ 𝐴 ∧ ∪ (𝐹‘𝑘) ≈ 1o)) ∧ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))
135	133, 134	eqeltrrd 2842	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑘 ∈ 𝐴 ∧ ∪ (𝐹‘𝑘) ≈ 1o)) ∧ 𝑦 ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → ∪ ∪ (𝐹‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))
136	126, 135	exlimddv 1935	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑘 ∈ 𝐴 ∧ ∪ (𝐹‘𝑘) ≈ 1o)) → ∪ ∪ (𝐹‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))
137	136	adantlr 715	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}⟶V) ∧ (𝑘 ∈ 𝐴 ∧ ∪ (𝐹‘𝑘) ≈ 1o)) → ∪ ∪ (𝐹‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))
138	125, 137	eqeltrd 2841	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}⟶V) ∧ (𝑘 ∈ 𝐴 ∧ ∪ (𝐹‘𝑘) ≈ 1o)) → if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))
139	138	a1d 25	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}⟶V) ∧ (𝑘 ∈ 𝐴 ∧ ∪ (𝐹‘𝑘) ≈ 1o)) → ((¬ ∪ (𝐹‘𝑘) ≈ 1o → (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)))
140	139	expr 456	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}⟶V) ∧ 𝑘 ∈ 𝐴) → (∪ (𝐹‘𝑘) ≈ 1o → ((¬ ∪ (𝐹‘𝑘) ≈ 1o → (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))))
141		pm2.27 42	. . . . . . . 8 ⊢ (¬ ∪ (𝐹‘𝑘) ≈ 1o → ((¬ ∪ (𝐹‘𝑘) ≈ 1o → (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)))
142		iffalse 4534	. . . . . . . . 9 ⊢ (¬ ∪ (𝐹‘𝑘) ≈ 1o → if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) = (𝑔‘𝑘))
143	142	eleq1d 2826	. . . . . . . 8 ⊢ (¬ ∪ (𝐹‘𝑘) ≈ 1o → (if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾) ↔ (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)))
144	141, 143	sylibrd 259	. . . . . . 7 ⊢ (¬ ∪ (𝐹‘𝑘) ≈ 1o → ((¬ ∪ (𝐹‘𝑘) ≈ 1o → (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)))
145	140, 144	pm2.61d1 180	. . . . . 6 ⊢ (((𝜑 ∧ 𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}⟶V) ∧ 𝑘 ∈ 𝐴) → ((¬ ∪ (𝐹‘𝑘) ≈ 1o → (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)))
146	145	ralimdva 3167	. . . . 5 ⊢ ((𝜑 ∧ 𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}⟶V) → (∀𝑘 ∈ 𝐴 (¬ ∪ (𝐹‘𝑘) ≈ 1o → (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → ∀𝑘 ∈ 𝐴 if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)))
147	123, 146	biimtrid 242	. . . 4 ⊢ ((𝜑 ∧ 𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}⟶V) → (∀𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o} (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾) → ∀𝑘 ∈ 𝐴 if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)))
148	147	impr 454	. . 3 ⊢ ((𝜑 ∧ (𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}⟶V ∧ ∀𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o} (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))) → ∀𝑘 ∈ 𝐴 if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))
149		fneq1 6659	. . . . . 6 ⊢ (𝑓 = (𝑚 ∈ 𝐴 ↦ if(∪ (𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) → (𝑓 Fn 𝐴 ↔ (𝑚 ∈ 𝐴 ↦ if(∪ (𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) Fn 𝐴))
150		fveq1 6905	. . . . . . . . 9 ⊢ (𝑓 = (𝑚 ∈ 𝐴 ↦ if(∪ (𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) → (𝑓‘𝑘) = ((𝑚 ∈ 𝐴 ↦ if(∪ (𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚)))‘𝑘))
151		fveq2 6906	. . . . . . . . . . . . 13 ⊢ (𝑚 = 𝑘 → (𝐹‘𝑚) = (𝐹‘𝑘))
152	151	unieqd 4920	. . . . . . . . . . . 12 ⊢ (𝑚 = 𝑘 → ∪ (𝐹‘𝑚) = ∪ (𝐹‘𝑘))
153	152	breq1d 5153	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑘 → (∪ (𝐹‘𝑚) ≈ 1o ↔ ∪ (𝐹‘𝑘) ≈ 1o))
154	152	unieqd 4920	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑘 → ∪ ∪ (𝐹‘𝑚) = ∪ ∪ (𝐹‘𝑘))
155		fveq2 6906	. . . . . . . . . . 11 ⊢ (𝑚 = 𝑘 → (𝑔‘𝑚) = (𝑔‘𝑘))
156	153, 154, 155	ifbieq12d 4554	. . . . . . . . . 10 ⊢ (𝑚 = 𝑘 → if(∪ (𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚)) = if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)))
157		fvex 6919	. . . . . . . . . . . . 13 ⊢ (𝐹‘𝑘) ∈ V
158	157	uniex 7761	. . . . . . . . . . . 12 ⊢ ∪ (𝐹‘𝑘) ∈ V
159	158	uniex 7761	. . . . . . . . . . 11 ⊢ ∪ ∪ (𝐹‘𝑘) ∈ V
160		fvex 6919	. . . . . . . . . . 11 ⊢ (𝑔‘𝑘) ∈ V
161	159, 160	ifex 4576	. . . . . . . . . 10 ⊢ if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ V
162	156, 118, 161	fvmpt 7016	. . . . . . . . 9 ⊢ (𝑘 ∈ 𝐴 → ((𝑚 ∈ 𝐴 ↦ if(∪ (𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚)))‘𝑘) = if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)))
163	150, 162	sylan9eq 2797	. . . . . . . 8 ⊢ ((𝑓 = (𝑚 ∈ 𝐴 ↦ if(∪ (𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) ∧ 𝑘 ∈ 𝐴) → (𝑓‘𝑘) = if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)))
164	163	eleq1d 2826	. . . . . . 7 ⊢ ((𝑓 = (𝑚 ∈ 𝐴 ↦ if(∪ (𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) ∧ 𝑘 ∈ 𝐴) → ((𝑓‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾) ↔ if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)))
165	164	ralbidva 3176	. . . . . 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 1117	. . 3 ⊢ (((𝑚 ∈ 𝐴 ↦ if(∪ (𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) ∈ V ∧ (𝑚 ∈ 𝐴 ↦ if(∪ (𝐹‘𝑚) ≈ 1o, ∪ ∪ (𝐹‘𝑚), (𝑔‘𝑚))) Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 if(∪ (𝐹‘𝑘) ≈ 1o, ∪ ∪ (𝐹‘𝑘), (𝑔‘𝑘)) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)) → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (𝑓‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)))
169	111, 120, 148, 168	syl3anc 1373	. 2 ⊢ ((𝜑 ∧ (𝑔:{𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o}⟶V ∧ ∀𝑘 ∈ {𝑛 ∈ 𝐴 ∣ ¬ ∪ (𝐹‘𝑛) ≈ 1o} (𝑔‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾))) → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (𝑓‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)))
170	109, 169	exlimddv 1935	1 ⊢ (𝜑 → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑘 ∈ 𝐴 (𝑓‘𝑘) ∈ (∪ (𝐹‘𝑘) ∖ ∪ 𝐾)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540  ∃wex 1779   ∈ wcel 2108  {cab 2714  ∀wral 3061  ∃wrex 3070  {crab 3436  Vcvv 3480   ∖ cdif 3948   ∩ cin 3950   ⊆ wss 3951  ∅c0 4333  ifcif 4525  𝒫 cpw 4600  {csn 4626  ∪ cuni 4907  ∪ ciun 4991   class class class wbr 5143   ↦ cmpt 5225  ^◡ccnv 5684  dom cdm 5685  ran crn 5686   “ cima 5688   Fn wfn 6556  ⟶wf 6557  ‘cfv 6561   ∈ cmpo 7433  1_oc1o 8499  Xcixp 8937   ≈ cen 8982  Fincfn 8985  cardccrd 9975  Compccmp 23394  UFLcufl 23908

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-int 4947  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-se 5638  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-isom 6570  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1st 8014  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-1o 8506  df-oadd 8510  df-omul 8511  df-er 8745  df-map 8868  df-ixp 8938  df-en 8986  df-dom 8987  df-fin 8989  df-wdom 9605  df-card 9979  df-acn 9982  df-cmp 23395

This theorem is referenced by:  ptcmplem4  24063