ptcmplem3

	Ref	Expression
Hypotheses	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	ptcmplem3	⊢ ( 𝜑 → ∃ 𝑓 ( 𝑓 Fn 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑓 ‘ 𝑘 ) ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ptcmp.1	⊢ 𝑆 = ( 𝑘 ∈ 𝐴 , 𝑢 ∈ ( 𝐹 ‘ 𝑘 ) ↦ ( ^◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) )
2		ptcmp.2	⊢ 𝑋 = X 𝑛 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑛 )
3		ptcmp.3	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
4		ptcmp.4	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ Comp )
5		ptcmp.5	⊢ ( 𝜑 → 𝑋 ∈ ( UFL ∩ dom card ) )
6		ptcmplem2.5	⊢ ( 𝜑 → 𝑈 ⊆ ran 𝑆 )
7		ptcmplem2.6	⊢ ( 𝜑 → 𝑋 = ∪ 𝑈 )
8		ptcmplem2.7	⊢ ( 𝜑 → ¬ ∃ 𝑧 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝑋 = ∪ 𝑧 )
9		ptcmplem3.8	⊢ 𝐾 = { 𝑢 ∈ ( 𝐹 ‘ 𝑘 ) ∣ ( ^◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ∈ 𝑈 }
10		rabexg	⊢ ( 𝐴 ∈ 𝑉 → { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1_o } ∈ V )
11	3 10	syl	⊢ ( 𝜑 → { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1_o } ∈ V )
12	1 2 3 4 5 6 7 8	ptcmplem2	⊢ ( 𝜑 → ∪ 𝑘 ∈ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1_o } ∪ ( 𝐹 ‘ 𝑘 ) ∈ dom card )
13		eldifi	⊢ ( 𝑦 ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) → 𝑦 ∈ ∪ ( 𝐹 ‘ 𝑘 ) )
14	13	3ad2ant3	⊢ ( ( 𝜑 ∧ 𝑦 ∈ V ∧ 𝑦 ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) ) → 𝑦 ∈ ∪ ( 𝐹 ‘ 𝑘 ) )
15	14	rabssdv	⊢ ( 𝜑 → { 𝑦 ∈ V ∣ 𝑦 ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) } ⊆ ∪ ( 𝐹 ‘ 𝑘 ) )
16	15	ralrimivw	⊢ ( 𝜑 → ∀ 𝑘 ∈ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1_o } { 𝑦 ∈ V ∣ 𝑦 ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) } ⊆ ∪ ( 𝐹 ‘ 𝑘 ) )
17		ss2iun	⊢ ( ∀ 𝑘 ∈ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1_o } { 𝑦 ∈ V ∣ 𝑦 ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) } ⊆ ∪ ( 𝐹 ‘ 𝑘 ) → ∪ 𝑘 ∈ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1_o } { 𝑦 ∈ V ∣ 𝑦 ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) } ⊆ ∪ 𝑘 ∈ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1_o } ∪ ( 𝐹 ‘ 𝑘 ) )
18	16 17	syl	⊢ ( 𝜑 → ∪ 𝑘 ∈ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1_o } { 𝑦 ∈ V ∣ 𝑦 ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) } ⊆ ∪ 𝑘 ∈ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1_o } ∪ ( 𝐹 ‘ 𝑘 ) )
19		ssnum	⊢ ( ( ∪ 𝑘 ∈ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1_o } ∪ ( 𝐹 ‘ 𝑘 ) ∈ dom card ∧ ∪ 𝑘 ∈ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1_o } { 𝑦 ∈ V ∣ 𝑦 ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) } ⊆ ∪ 𝑘 ∈ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1_o } ∪ ( 𝐹 ‘ 𝑘 ) ) → ∪ 𝑘 ∈ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1_o } { 𝑦 ∈ V ∣ 𝑦 ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) } ∈ dom card )
20	12 18 19	syl2anc	⊢ ( 𝜑 → ∪ 𝑘 ∈ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1_o } { 𝑦 ∈ V ∣ 𝑦 ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) } ∈ dom card )
21		elrabi	⊢ ( 𝑘 ∈ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1_o } → 𝑘 ∈ 𝐴 )
22	8	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ¬ ∃ 𝑧 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝑋 = ∪ 𝑧 )
23		ssdif0	⊢ ( ∪ ( 𝐹 ‘ 𝑘 ) ⊆ ∪ 𝐾 ↔ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) = ∅ )
24	4	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑘 ) ∈ Comp )
25	24	adantr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ ∪ ( 𝐹 ‘ 𝑘 ) ⊆ ∪ 𝐾 ) → ( 𝐹 ‘ 𝑘 ) ∈ Comp )
26	9	ssrab3	⊢ 𝐾 ⊆ ( 𝐹 ‘ 𝑘 )
27	26	a1i	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ ∪ ( 𝐹 ‘ 𝑘 ) ⊆ ∪ 𝐾 ) → 𝐾 ⊆ ( 𝐹 ‘ 𝑘 ) )
28		simpr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ ∪ ( 𝐹 ‘ 𝑘 ) ⊆ ∪ 𝐾 ) → ∪ ( 𝐹 ‘ 𝑘 ) ⊆ ∪ 𝐾 )
29		uniss	⊢ ( 𝐾 ⊆ ( 𝐹 ‘ 𝑘 ) → ∪ 𝐾 ⊆ ∪ ( 𝐹 ‘ 𝑘 ) )
30	26 29	mp1i	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ ∪ ( 𝐹 ‘ 𝑘 ) ⊆ ∪ 𝐾 ) → ∪ 𝐾 ⊆ ∪ ( 𝐹 ‘ 𝑘 ) )
31	28 30	eqssd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ ∪ ( 𝐹 ‘ 𝑘 ) ⊆ ∪ 𝐾 ) → ∪ ( 𝐹 ‘ 𝑘 ) = ∪ 𝐾 )
32		eqid	⊢ ∪ ( 𝐹 ‘ 𝑘 ) = ∪ ( 𝐹 ‘ 𝑘 )
33	32	cmpcov	⊢ ( ( ( 𝐹 ‘ 𝑘 ) ∈ Comp ∧ 𝐾 ⊆ ( 𝐹 ‘ 𝑘 ) ∧ ∪ ( 𝐹 ‘ 𝑘 ) = ∪ 𝐾 ) → ∃ 𝑡 ∈ ( 𝒫 𝐾 ∩ Fin ) ∪ ( 𝐹 ‘ 𝑘 ) = ∪ 𝑡 )
34	25 27 31 33	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ ∪ ( 𝐹 ‘ 𝑘 ) ⊆ ∪ 𝐾 ) → ∃ 𝑡 ∈ ( 𝒫 𝐾 ∩ Fin ) ∪ ( 𝐹 ‘ 𝑘 ) = ∪ 𝑡 )
35		elfpw	⊢ ( 𝑡 ∈ ( 𝒫 𝐾 ∩ Fin ) ↔ ( 𝑡 ⊆ 𝐾 ∧ 𝑡 ∈ Fin ) )
36	35	simplbi	⊢ ( 𝑡 ∈ ( 𝒫 𝐾 ∩ Fin ) → 𝑡 ⊆ 𝐾 )
37	36	ad2antrl	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ ∪ ( 𝐹 ‘ 𝑘 ) ⊆ ∪ 𝐾 ) ∧ ( 𝑡 ∈ ( 𝒫 𝐾 ∩ Fin ) ∧ ∪ ( 𝐹 ‘ 𝑘 ) = ∪ 𝑡 ) ) → 𝑡 ⊆ 𝐾 )
38	37	sselda	⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ ∪ ( 𝐹 ‘ 𝑘 ) ⊆ ∪ 𝐾 ) ∧ ( 𝑡 ∈ ( 𝒫 𝐾 ∩ Fin ) ∧ ∪ ( 𝐹 ‘ 𝑘 ) = ∪ 𝑡 ) ) ∧ 𝑥 ∈ 𝑡 ) → 𝑥 ∈ 𝐾 )
39		imaeq2	⊢ ( 𝑢 = 𝑥 → ( ^◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) = ( ^◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑥 ) )
40	39	eleq1d	⊢ ( 𝑢 = 𝑥 → ( ( ^◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ∈ 𝑈 ↔ ( ^◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑥 ) ∈ 𝑈 ) )
41	40 9	elrab2	⊢ ( 𝑥 ∈ 𝐾 ↔ ( 𝑥 ∈ ( 𝐹 ‘ 𝑘 ) ∧ ( ^◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑥 ) ∈ 𝑈 ) )
42	41	simprbi	⊢ ( 𝑥 ∈ 𝐾 → ( ^◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑥 ) ∈ 𝑈 )
43	38 42	syl	⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ ∪ ( 𝐹 ‘ 𝑘 ) ⊆ ∪ 𝐾 ) ∧ ( 𝑡 ∈ ( 𝒫 𝐾 ∩ Fin ) ∧ ∪ ( 𝐹 ‘ 𝑘 ) = ∪ 𝑡 ) ) ∧ 𝑥 ∈ 𝑡 ) → ( ^◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑥 ) ∈ 𝑈 )
44	43	fmpttd	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ ∪ ( 𝐹 ‘ 𝑘 ) ⊆ ∪ 𝐾 ) ∧ ( 𝑡 ∈ ( 𝒫 𝐾 ∩ Fin ) ∧ ∪ ( 𝐹 ‘ 𝑘 ) = ∪ 𝑡 ) ) → ( 𝑥 ∈ 𝑡 ↦ ( ^◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑥 ) ) : 𝑡 ⟶ 𝑈 )
45	44	frnd	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ ∪ ( 𝐹 ‘ 𝑘 ) ⊆ ∪ 𝐾 ) ∧ ( 𝑡 ∈ ( 𝒫 𝐾 ∩ Fin ) ∧ ∪ ( 𝐹 ‘ 𝑘 ) = ∪ 𝑡 ) ) → ran ( 𝑥 ∈ 𝑡 ↦ ( ^◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑥 ) ) ⊆ 𝑈 )
46	35	simprbi	⊢ ( 𝑡 ∈ ( 𝒫 𝐾 ∩ Fin ) → 𝑡 ∈ Fin )
47	46	ad2antrl	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ ∪ ( 𝐹 ‘ 𝑘 ) ⊆ ∪ 𝐾 ) ∧ ( 𝑡 ∈ ( 𝒫 𝐾 ∩ Fin ) ∧ ∪ ( 𝐹 ‘ 𝑘 ) = ∪ 𝑡 ) ) → 𝑡 ∈ Fin )
48		eqid	⊢ ( 𝑥 ∈ 𝑡 ↦ ( ^◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑥 ) ) = ( 𝑥 ∈ 𝑡 ↦ ( ^◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑥 ) )
49	48	rnmpt	⊢ ran ( 𝑥 ∈ 𝑡 ↦ ( ^◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑥 ) ) = { 𝑓 ∣ ∃ 𝑥 ∈ 𝑡 𝑓 = ( ^◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑥 ) }
50		abrexfi	⊢ ( 𝑡 ∈ Fin → { 𝑓 ∣ ∃ 𝑥 ∈ 𝑡 𝑓 = ( ^◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑥 ) } ∈ Fin )
51	49 50	eqeltrid	⊢ ( 𝑡 ∈ Fin → ran ( 𝑥 ∈ 𝑡 ↦ ( ^◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑥 ) ) ∈ Fin )
52	47 51	syl	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ ∪ ( 𝐹 ‘ 𝑘 ) ⊆ ∪ 𝐾 ) ∧ ( 𝑡 ∈ ( 𝒫 𝐾 ∩ Fin ) ∧ ∪ ( 𝐹 ‘ 𝑘 ) = ∪ 𝑡 ) ) → ran ( 𝑥 ∈ 𝑡 ↦ ( ^◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑥 ) ) ∈ Fin )
53		elfpw	⊢ ( ran ( 𝑥 ∈ 𝑡 ↦ ( ^◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑥 ) ) ∈ ( 𝒫 𝑈 ∩ Fin ) ↔ ( ran ( 𝑥 ∈ 𝑡 ↦ ( ^◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑥 ) ) ⊆ 𝑈 ∧ ran ( 𝑥 ∈ 𝑡 ↦ ( ^◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑥 ) ) ∈ Fin ) )
54	45 52 53	sylanbrc	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ ∪ ( 𝐹 ‘ 𝑘 ) ⊆ ∪ 𝐾 ) ∧ ( 𝑡 ∈ ( 𝒫 𝐾 ∩ Fin ) ∧ ∪ ( 𝐹 ‘ 𝑘 ) = ∪ 𝑡 ) ) → ran ( 𝑥 ∈ 𝑡 ↦ ( ^◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑥 ) ) ∈ ( 𝒫 𝑈 ∩ Fin ) )
55		fveq2	⊢ ( 𝑛 = 𝑘 → ( 𝑓 ‘ 𝑛 ) = ( 𝑓 ‘ 𝑘 ) )
56		fveq2	⊢ ( 𝑛 = 𝑘 → ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑘 ) )
57	56	unieqd	⊢ ( 𝑛 = 𝑘 → ∪ ( 𝐹 ‘ 𝑛 ) = ∪ ( 𝐹 ‘ 𝑘 ) )
58	55 57	eleq12d	⊢ ( 𝑛 = 𝑘 → ( ( 𝑓 ‘ 𝑛 ) ∈ ∪ ( 𝐹 ‘ 𝑛 ) ↔ ( 𝑓 ‘ 𝑘 ) ∈ ∪ ( 𝐹 ‘ 𝑘 ) ) )
59		simpr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ ∪ ( 𝐹 ‘ 𝑘 ) ⊆ ∪ 𝐾 ) ∧ ( 𝑡 ∈ ( 𝒫 𝐾 ∩ Fin ) ∧ ∪ ( 𝐹 ‘ 𝑘 ) = ∪ 𝑡 ) ) ∧ 𝑓 ∈ 𝑋 ) → 𝑓 ∈ 𝑋 )
60	59 2	eleqtrdi	⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ ∪ ( 𝐹 ‘ 𝑘 ) ⊆ ∪ 𝐾 ) ∧ ( 𝑡 ∈ ( 𝒫 𝐾 ∩ Fin ) ∧ ∪ ( 𝐹 ‘ 𝑘 ) = ∪ 𝑡 ) ) ∧ 𝑓 ∈ 𝑋 ) → 𝑓 ∈ X 𝑛 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑛 ) )
61		vex	⊢ 𝑓 ∈ V
62	61	elixp	⊢ ( 𝑓 ∈ X 𝑛 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑛 ) ↔ ( 𝑓 Fn 𝐴 ∧ ∀ 𝑛 ∈ 𝐴 ( 𝑓 ‘ 𝑛 ) ∈ ∪ ( 𝐹 ‘ 𝑛 ) ) )
63	62	simprbi	⊢ ( 𝑓 ∈ X 𝑛 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑛 ) → ∀ 𝑛 ∈ 𝐴 ( 𝑓 ‘ 𝑛 ) ∈ ∪ ( 𝐹 ‘ 𝑛 ) )
64	60 63	syl	⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ ∪ ( 𝐹 ‘ 𝑘 ) ⊆ ∪ 𝐾 ) ∧ ( 𝑡 ∈ ( 𝒫 𝐾 ∩ Fin ) ∧ ∪ ( 𝐹 ‘ 𝑘 ) = ∪ 𝑡 ) ) ∧ 𝑓 ∈ 𝑋 ) → ∀ 𝑛 ∈ 𝐴 ( 𝑓 ‘ 𝑛 ) ∈ ∪ ( 𝐹 ‘ 𝑛 ) )
65		simp-4r	⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ ∪ ( 𝐹 ‘ 𝑘 ) ⊆ ∪ 𝐾 ) ∧ ( 𝑡 ∈ ( 𝒫 𝐾 ∩ Fin ) ∧ ∪ ( 𝐹 ‘ 𝑘 ) = ∪ 𝑡 ) ) ∧ 𝑓 ∈ 𝑋 ) → 𝑘 ∈ 𝐴 )
66	58 64 65	rspcdva	⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ ∪ ( 𝐹 ‘ 𝑘 ) ⊆ ∪ 𝐾 ) ∧ ( 𝑡 ∈ ( 𝒫 𝐾 ∩ Fin ) ∧ ∪ ( 𝐹 ‘ 𝑘 ) = ∪ 𝑡 ) ) ∧ 𝑓 ∈ 𝑋 ) → ( 𝑓 ‘ 𝑘 ) ∈ ∪ ( 𝐹 ‘ 𝑘 ) )
67		simplrr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ ∪ ( 𝐹 ‘ 𝑘 ) ⊆ ∪ 𝐾 ) ∧ ( 𝑡 ∈ ( 𝒫 𝐾 ∩ Fin ) ∧ ∪ ( 𝐹 ‘ 𝑘 ) = ∪ 𝑡 ) ) ∧ 𝑓 ∈ 𝑋 ) → ∪ ( 𝐹 ‘ 𝑘 ) = ∪ 𝑡 )
68	66 67	eleqtrd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ ∪ ( 𝐹 ‘ 𝑘 ) ⊆ ∪ 𝐾 ) ∧ ( 𝑡 ∈ ( 𝒫 𝐾 ∩ Fin ) ∧ ∪ ( 𝐹 ‘ 𝑘 ) = ∪ 𝑡 ) ) ∧ 𝑓 ∈ 𝑋 ) → ( 𝑓 ‘ 𝑘 ) ∈ ∪ 𝑡 )
69		eluni2	⊢ ( ( 𝑓 ‘ 𝑘 ) ∈ ∪ 𝑡 ↔ ∃ 𝑥 ∈ 𝑡 ( 𝑓 ‘ 𝑘 ) ∈ 𝑥 )
70	68 69	sylib	⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ ∪ ( 𝐹 ‘ 𝑘 ) ⊆ ∪ 𝐾 ) ∧ ( 𝑡 ∈ ( 𝒫 𝐾 ∩ Fin ) ∧ ∪ ( 𝐹 ‘ 𝑘 ) = ∪ 𝑡 ) ) ∧ 𝑓 ∈ 𝑋 ) → ∃ 𝑥 ∈ 𝑡 ( 𝑓 ‘ 𝑘 ) ∈ 𝑥 )
71		fveq1	⊢ ( 𝑤 = 𝑓 → ( 𝑤 ‘ 𝑘 ) = ( 𝑓 ‘ 𝑘 ) )
72	71	eleq1d	⊢ ( 𝑤 = 𝑓 → ( ( 𝑤 ‘ 𝑘 ) ∈ 𝑥 ↔ ( 𝑓 ‘ 𝑘 ) ∈ 𝑥 ) )
73		eqid	⊢ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) = ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) )
74	73	mptpreima	⊢ ( ^◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑥 ) = { 𝑤 ∈ 𝑋 ∣ ( 𝑤 ‘ 𝑘 ) ∈ 𝑥 }
75	72 74	elrab2	⊢ ( 𝑓 ∈ ( ^◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑥 ) ↔ ( 𝑓 ∈ 𝑋 ∧ ( 𝑓 ‘ 𝑘 ) ∈ 𝑥 ) )
76	75	baib	⊢ ( 𝑓 ∈ 𝑋 → ( 𝑓 ∈ ( ^◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑥 ) ↔ ( 𝑓 ‘ 𝑘 ) ∈ 𝑥 ) )
77	76	ad2antlr	⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ ∪ ( 𝐹 ‘ 𝑘 ) ⊆ ∪ 𝐾 ) ∧ ( 𝑡 ∈ ( 𝒫 𝐾 ∩ Fin ) ∧ ∪ ( 𝐹 ‘ 𝑘 ) = ∪ 𝑡 ) ) ∧ 𝑓 ∈ 𝑋 ) ∧ 𝑥 ∈ 𝑡 ) → ( 𝑓 ∈ ( ^◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑥 ) ↔ ( 𝑓 ‘ 𝑘 ) ∈ 𝑥 ) )
78	77	rexbidva	⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ ∪ ( 𝐹 ‘ 𝑘 ) ⊆ ∪ 𝐾 ) ∧ ( 𝑡 ∈ ( 𝒫 𝐾 ∩ Fin ) ∧ ∪ ( 𝐹 ‘ 𝑘 ) = ∪ 𝑡 ) ) ∧ 𝑓 ∈ 𝑋 ) → ( ∃ 𝑥 ∈ 𝑡 𝑓 ∈ ( ^◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑥 ) ↔ ∃ 𝑥 ∈ 𝑡 ( 𝑓 ‘ 𝑘 ) ∈ 𝑥 ) )
79	70 78	mpbird	⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ ∪ ( 𝐹 ‘ 𝑘 ) ⊆ ∪ 𝐾 ) ∧ ( 𝑡 ∈ ( 𝒫 𝐾 ∩ Fin ) ∧ ∪ ( 𝐹 ‘ 𝑘 ) = ∪ 𝑡 ) ) ∧ 𝑓 ∈ 𝑋 ) → ∃ 𝑥 ∈ 𝑡 𝑓 ∈ ( ^◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑥 ) )
80		eliun	⊢ ( 𝑓 ∈ ∪ 𝑥 ∈ 𝑡 ( ^◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑥 ) ↔ ∃ 𝑥 ∈ 𝑡 𝑓 ∈ ( ^◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑥 ) )
81	79 80	sylibr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ ∪ ( 𝐹 ‘ 𝑘 ) ⊆ ∪ 𝐾 ) ∧ ( 𝑡 ∈ ( 𝒫 𝐾 ∩ Fin ) ∧ ∪ ( 𝐹 ‘ 𝑘 ) = ∪ 𝑡 ) ) ∧ 𝑓 ∈ 𝑋 ) → 𝑓 ∈ ∪ 𝑥 ∈ 𝑡 ( ^◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑥 ) )
82	81	ex	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ ∪ ( 𝐹 ‘ 𝑘 ) ⊆ ∪ 𝐾 ) ∧ ( 𝑡 ∈ ( 𝒫 𝐾 ∩ Fin ) ∧ ∪ ( 𝐹 ‘ 𝑘 ) = ∪ 𝑡 ) ) → ( 𝑓 ∈ 𝑋 → 𝑓 ∈ ∪ 𝑥 ∈ 𝑡 ( ^◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑥 ) ) )
83	82	ssrdv	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ ∪ ( 𝐹 ‘ 𝑘 ) ⊆ ∪ 𝐾 ) ∧ ( 𝑡 ∈ ( 𝒫 𝐾 ∩ Fin ) ∧ ∪ ( 𝐹 ‘ 𝑘 ) = ∪ 𝑡 ) ) → 𝑋 ⊆ ∪ 𝑥 ∈ 𝑡 ( ^◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑥 ) )
84	43	ralrimiva	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ ∪ ( 𝐹 ‘ 𝑘 ) ⊆ ∪ 𝐾 ) ∧ ( 𝑡 ∈ ( 𝒫 𝐾 ∩ Fin ) ∧ ∪ ( 𝐹 ‘ 𝑘 ) = ∪ 𝑡 ) ) → ∀ 𝑥 ∈ 𝑡 ( ^◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑥 ) ∈ 𝑈 )
85		dfiun2g	⊢ ( ∀ 𝑥 ∈ 𝑡 ( ^◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑥 ) ∈ 𝑈 → ∪ 𝑥 ∈ 𝑡 ( ^◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑥 ) = ∪ { 𝑓 ∣ ∃ 𝑥 ∈ 𝑡 𝑓 = ( ^◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑥 ) } )
86	84 85	syl	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ ∪ ( 𝐹 ‘ 𝑘 ) ⊆ ∪ 𝐾 ) ∧ ( 𝑡 ∈ ( 𝒫 𝐾 ∩ Fin ) ∧ ∪ ( 𝐹 ‘ 𝑘 ) = ∪ 𝑡 ) ) → ∪ 𝑥 ∈ 𝑡 ( ^◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑥 ) = ∪ { 𝑓 ∣ ∃ 𝑥 ∈ 𝑡 𝑓 = ( ^◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑥 ) } )
87	49	unieqi	⊢ ∪ ran ( 𝑥 ∈ 𝑡 ↦ ( ^◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑥 ) ) = ∪ { 𝑓 ∣ ∃ 𝑥 ∈ 𝑡 𝑓 = ( ^◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑥 ) }
88	86 87	eqtr4di	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ ∪ ( 𝐹 ‘ 𝑘 ) ⊆ ∪ 𝐾 ) ∧ ( 𝑡 ∈ ( 𝒫 𝐾 ∩ Fin ) ∧ ∪ ( 𝐹 ‘ 𝑘 ) = ∪ 𝑡 ) ) → ∪ 𝑥 ∈ 𝑡 ( ^◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑥 ) = ∪ ran ( 𝑥 ∈ 𝑡 ↦ ( ^◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑥 ) ) )
89	83 88	sseqtrd	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ ∪ ( 𝐹 ‘ 𝑘 ) ⊆ ∪ 𝐾 ) ∧ ( 𝑡 ∈ ( 𝒫 𝐾 ∩ Fin ) ∧ ∪ ( 𝐹 ‘ 𝑘 ) = ∪ 𝑡 ) ) → 𝑋 ⊆ ∪ ran ( 𝑥 ∈ 𝑡 ↦ ( ^◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑥 ) ) )
90	45	unissd	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ ∪ ( 𝐹 ‘ 𝑘 ) ⊆ ∪ 𝐾 ) ∧ ( 𝑡 ∈ ( 𝒫 𝐾 ∩ Fin ) ∧ ∪ ( 𝐹 ‘ 𝑘 ) = ∪ 𝑡 ) ) → ∪ ran ( 𝑥 ∈ 𝑡 ↦ ( ^◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑥 ) ) ⊆ ∪ 𝑈 )
91	7	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ ∪ ( 𝐹 ‘ 𝑘 ) ⊆ ∪ 𝐾 ) ∧ ( 𝑡 ∈ ( 𝒫 𝐾 ∩ Fin ) ∧ ∪ ( 𝐹 ‘ 𝑘 ) = ∪ 𝑡 ) ) → 𝑋 = ∪ 𝑈 )
92	90 91	sseqtrrd	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ ∪ ( 𝐹 ‘ 𝑘 ) ⊆ ∪ 𝐾 ) ∧ ( 𝑡 ∈ ( 𝒫 𝐾 ∩ Fin ) ∧ ∪ ( 𝐹 ‘ 𝑘 ) = ∪ 𝑡 ) ) → ∪ ran ( 𝑥 ∈ 𝑡 ↦ ( ^◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑥 ) ) ⊆ 𝑋 )
93	89 92	eqssd	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ ∪ ( 𝐹 ‘ 𝑘 ) ⊆ ∪ 𝐾 ) ∧ ( 𝑡 ∈ ( 𝒫 𝐾 ∩ Fin ) ∧ ∪ ( 𝐹 ‘ 𝑘 ) = ∪ 𝑡 ) ) → 𝑋 = ∪ ran ( 𝑥 ∈ 𝑡 ↦ ( ^◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑥 ) ) )
94		unieq	⊢ ( 𝑧 = ran ( 𝑥 ∈ 𝑡 ↦ ( ^◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑥 ) ) → ∪ 𝑧 = ∪ ran ( 𝑥 ∈ 𝑡 ↦ ( ^◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑥 ) ) )
95	94	rspceeqv	⊢ ( ( ran ( 𝑥 ∈ 𝑡 ↦ ( ^◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑥 ) ) ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ 𝑋 = ∪ ran ( 𝑥 ∈ 𝑡 ↦ ( ^◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑥 ) ) ) → ∃ 𝑧 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝑋 = ∪ 𝑧 )
96	54 93 95	syl2anc	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ ∪ ( 𝐹 ‘ 𝑘 ) ⊆ ∪ 𝐾 ) ∧ ( 𝑡 ∈ ( 𝒫 𝐾 ∩ Fin ) ∧ ∪ ( 𝐹 ‘ 𝑘 ) = ∪ 𝑡 ) ) → ∃ 𝑧 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝑋 = ∪ 𝑧 )
97	34 96	rexlimddv	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ ∪ ( 𝐹 ‘ 𝑘 ) ⊆ ∪ 𝐾 ) → ∃ 𝑧 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝑋 = ∪ 𝑧 )
98	97	ex	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( ∪ ( 𝐹 ‘ 𝑘 ) ⊆ ∪ 𝐾 → ∃ 𝑧 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝑋 = ∪ 𝑧 ) )
99	23 98	syl5bir	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) = ∅ → ∃ 𝑧 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝑋 = ∪ 𝑧 ) )
100	22 99	mtod	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ¬ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) = ∅ )
101		neq0	⊢ ( ¬ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) = ∅ ↔ ∃ 𝑦 𝑦 ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) )
102	100 101	sylib	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ∃ 𝑦 𝑦 ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) )
103		rexv	⊢ ( ∃ 𝑦 ∈ V 𝑦 ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) ↔ ∃ 𝑦 𝑦 ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) )
104	102 103	sylibr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ∃ 𝑦 ∈ V 𝑦 ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) )
105	21 104	sylan2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1_o } ) → ∃ 𝑦 ∈ V 𝑦 ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) )
106	105	ralrimiva	⊢ ( 𝜑 → ∀ 𝑘 ∈ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1_o } ∃ 𝑦 ∈ V 𝑦 ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) )
107		eleq1	⊢ ( 𝑦 = ( 𝑔 ‘ 𝑘 ) → ( 𝑦 ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) ↔ ( 𝑔 ‘ 𝑘 ) ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) ) )
108	107	ac6num	⊢ ( ( { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1_o } ∈ V ∧ ∪ 𝑘 ∈ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1_o } { 𝑦 ∈ V ∣ 𝑦 ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) } ∈ dom card ∧ ∀ 𝑘 ∈ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1_o } ∃ 𝑦 ∈ V 𝑦 ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) ) → ∃ 𝑔 ( 𝑔 : { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1_o } ⟶ V ∧ ∀ 𝑘 ∈ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1_o } ( 𝑔 ‘ 𝑘 ) ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) ) )
109	11 20 106 108	syl3anc	⊢ ( 𝜑 → ∃ 𝑔 ( 𝑔 : { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1_o } ⟶ V ∧ ∀ 𝑘 ∈ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1_o } ( 𝑔 ‘ 𝑘 ) ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) ) )
110	3	adantr	⊢ ( ( 𝜑 ∧ ( 𝑔 : { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1_o } ⟶ V ∧ ∀ 𝑘 ∈ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1_o } ( 𝑔 ‘ 𝑘 ) ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) ) ) → 𝐴 ∈ 𝑉 )
111	110	mptexd	⊢ ( ( 𝜑 ∧ ( 𝑔 : { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1_o } ⟶ V ∧ ∀ 𝑘 ∈ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1_o } ( 𝑔 ‘ 𝑘 ) ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) ) ) → ( 𝑚 ∈ 𝐴 ↦ if ( ∪ ( 𝐹 ‘ 𝑚 ) ≈ 1_o , ∪ ∪ ( 𝐹 ‘ 𝑚 ) , ( 𝑔 ‘ 𝑚 ) ) ) ∈ V )
112		fvex	⊢ ( 𝐹 ‘ 𝑚 ) ∈ V
113	112	uniex	⊢ ∪ ( 𝐹 ‘ 𝑚 ) ∈ V
114	113	uniex	⊢ ∪ ∪ ( 𝐹 ‘ 𝑚 ) ∈ V
115		fvex	⊢ ( 𝑔 ‘ 𝑚 ) ∈ V
116	114 115	ifex	⊢ if ( ∪ ( 𝐹 ‘ 𝑚 ) ≈ 1_o , ∪ ∪ ( 𝐹 ‘ 𝑚 ) , ( 𝑔 ‘ 𝑚 ) ) ∈ V
117	116	rgenw	⊢ ∀ 𝑚 ∈ 𝐴 if ( ∪ ( 𝐹 ‘ 𝑚 ) ≈ 1_o , ∪ ∪ ( 𝐹 ‘ 𝑚 ) , ( 𝑔 ‘ 𝑚 ) ) ∈ V
118		eqid	⊢ ( 𝑚 ∈ 𝐴 ↦ if ( ∪ ( 𝐹 ‘ 𝑚 ) ≈ 1_o , ∪ ∪ ( 𝐹 ‘ 𝑚 ) , ( 𝑔 ‘ 𝑚 ) ) ) = ( 𝑚 ∈ 𝐴 ↦ if ( ∪ ( 𝐹 ‘ 𝑚 ) ≈ 1_o , ∪ ∪ ( 𝐹 ‘ 𝑚 ) , ( 𝑔 ‘ 𝑚 ) ) )
119	118	fnmpt	⊢ ( ∀ 𝑚 ∈ 𝐴 if ( ∪ ( 𝐹 ‘ 𝑚 ) ≈ 1_o , ∪ ∪ ( 𝐹 ‘ 𝑚 ) , ( 𝑔 ‘ 𝑚 ) ) ∈ V → ( 𝑚 ∈ 𝐴 ↦ if ( ∪ ( 𝐹 ‘ 𝑚 ) ≈ 1_o , ∪ ∪ ( 𝐹 ‘ 𝑚 ) , ( 𝑔 ‘ 𝑚 ) ) ) Fn 𝐴 )
120	117 119	mp1i	⊢ ( ( 𝜑 ∧ ( 𝑔 : { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1_o } ⟶ V ∧ ∀ 𝑘 ∈ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1_o } ( 𝑔 ‘ 𝑘 ) ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) ) ) → ( 𝑚 ∈ 𝐴 ↦ if ( ∪ ( 𝐹 ‘ 𝑚 ) ≈ 1_o , ∪ ∪ ( 𝐹 ‘ 𝑚 ) , ( 𝑔 ‘ 𝑚 ) ) ) Fn 𝐴 )
121	57	breq1d	⊢ ( 𝑛 = 𝑘 → ( ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1_o ↔ ∪ ( 𝐹 ‘ 𝑘 ) ≈ 1_o ) )
122	121	notbid	⊢ ( 𝑛 = 𝑘 → ( ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1_o ↔ ¬ ∪ ( 𝐹 ‘ 𝑘 ) ≈ 1_o ) )
123	122	ralrab	⊢ ( ∀ 𝑘 ∈ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1_o } ( 𝑔 ‘ 𝑘 ) ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) ↔ ∀ 𝑘 ∈ 𝐴 ( ¬ ∪ ( 𝐹 ‘ 𝑘 ) ≈ 1_o → ( 𝑔 ‘ 𝑘 ) ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) ) )
124		iftrue	⊢ ( ∪ ( 𝐹 ‘ 𝑘 ) ≈ 1_o → if ( ∪ ( 𝐹 ‘ 𝑘 ) ≈ 1_o , ∪ ∪ ( 𝐹 ‘ 𝑘 ) , ( 𝑔 ‘ 𝑘 ) ) = ∪ ∪ ( 𝐹 ‘ 𝑘 ) )
125	124	ad2antll	⊢ ( ( ( 𝜑 ∧ 𝑔 : { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1_o } ⟶ V ) ∧ ( 𝑘 ∈ 𝐴 ∧ ∪ ( 𝐹 ‘ 𝑘 ) ≈ 1_o ) ) → if ( ∪ ( 𝐹 ‘ 𝑘 ) ≈ 1_o , ∪ ∪ ( 𝐹 ‘ 𝑘 ) , ( 𝑔 ‘ 𝑘 ) ) = ∪ ∪ ( 𝐹 ‘ 𝑘 ) )
126	102	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝐴 ∧ ∪ ( 𝐹 ‘ 𝑘 ) ≈ 1_o ) ) → ∃ 𝑦 𝑦 ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) )
127	13	adantl	⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ 𝐴 ∧ ∪ ( 𝐹 ‘ 𝑘 ) ≈ 1_o ) ) ∧ 𝑦 ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) ) → 𝑦 ∈ ∪ ( 𝐹 ‘ 𝑘 ) )
128		simplrr	⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ 𝐴 ∧ ∪ ( 𝐹 ‘ 𝑘 ) ≈ 1_o ) ) ∧ 𝑦 ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) ) → ∪ ( 𝐹 ‘ 𝑘 ) ≈ 1_o )
129		en1b	⊢ ( ∪ ( 𝐹 ‘ 𝑘 ) ≈ 1_o ↔ ∪ ( 𝐹 ‘ 𝑘 ) = { ∪ ∪ ( 𝐹 ‘ 𝑘 ) } )
130	128 129	sylib	⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ 𝐴 ∧ ∪ ( 𝐹 ‘ 𝑘 ) ≈ 1_o ) ) ∧ 𝑦 ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) ) → ∪ ( 𝐹 ‘ 𝑘 ) = { ∪ ∪ ( 𝐹 ‘ 𝑘 ) } )
131	127 130	eleqtrd	⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ 𝐴 ∧ ∪ ( 𝐹 ‘ 𝑘 ) ≈ 1_o ) ) ∧ 𝑦 ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) ) → 𝑦 ∈ { ∪ ∪ ( 𝐹 ‘ 𝑘 ) } )
132		elsni	⊢ ( 𝑦 ∈ { ∪ ∪ ( 𝐹 ‘ 𝑘 ) } → 𝑦 = ∪ ∪ ( 𝐹 ‘ 𝑘 ) )
133	131 132	syl	⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ 𝐴 ∧ ∪ ( 𝐹 ‘ 𝑘 ) ≈ 1_o ) ) ∧ 𝑦 ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) ) → 𝑦 = ∪ ∪ ( 𝐹 ‘ 𝑘 ) )
134		simpr	⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ 𝐴 ∧ ∪ ( 𝐹 ‘ 𝑘 ) ≈ 1_o ) ) ∧ 𝑦 ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) ) → 𝑦 ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) )
135	133 134	eqeltrrd	⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ 𝐴 ∧ ∪ ( 𝐹 ‘ 𝑘 ) ≈ 1_o ) ) ∧ 𝑦 ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) ) → ∪ ∪ ( 𝐹 ‘ 𝑘 ) ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) )
136	126 135	exlimddv	⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝐴 ∧ ∪ ( 𝐹 ‘ 𝑘 ) ≈ 1_o ) ) → ∪ ∪ ( 𝐹 ‘ 𝑘 ) ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) )
137	136	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑔 : { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1_o } ⟶ V ) ∧ ( 𝑘 ∈ 𝐴 ∧ ∪ ( 𝐹 ‘ 𝑘 ) ≈ 1_o ) ) → ∪ ∪ ( 𝐹 ‘ 𝑘 ) ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) )
138	125 137	eqeltrd	⊢ ( ( ( 𝜑 ∧ 𝑔 : { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1_o } ⟶ V ) ∧ ( 𝑘 ∈ 𝐴 ∧ ∪ ( 𝐹 ‘ 𝑘 ) ≈ 1_o ) ) → if ( ∪ ( 𝐹 ‘ 𝑘 ) ≈ 1_o , ∪ ∪ ( 𝐹 ‘ 𝑘 ) , ( 𝑔 ‘ 𝑘 ) ) ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) )
139	138	a1d	⊢ ( ( ( 𝜑 ∧ 𝑔 : { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1_o } ⟶ V ) ∧ ( 𝑘 ∈ 𝐴 ∧ ∪ ( 𝐹 ‘ 𝑘 ) ≈ 1_o ) ) → ( ( ¬ ∪ ( 𝐹 ‘ 𝑘 ) ≈ 1_o → ( 𝑔 ‘ 𝑘 ) ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) ) → if ( ∪ ( 𝐹 ‘ 𝑘 ) ≈ 1_o , ∪ ∪ ( 𝐹 ‘ 𝑘 ) , ( 𝑔 ‘ 𝑘 ) ) ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) ) )
140	139	expr	⊢ ( ( ( 𝜑 ∧ 𝑔 : { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1_o } ⟶ V ) ∧ 𝑘 ∈ 𝐴 ) → ( ∪ ( 𝐹 ‘ 𝑘 ) ≈ 1_o → ( ( ¬ ∪ ( 𝐹 ‘ 𝑘 ) ≈ 1_o → ( 𝑔 ‘ 𝑘 ) ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) ) → if ( ∪ ( 𝐹 ‘ 𝑘 ) ≈ 1_o , ∪ ∪ ( 𝐹 ‘ 𝑘 ) , ( 𝑔 ‘ 𝑘 ) ) ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) ) ) )
141		pm2.27	⊢ ( ¬ ∪ ( 𝐹 ‘ 𝑘 ) ≈ 1_o → ( ( ¬ ∪ ( 𝐹 ‘ 𝑘 ) ≈ 1_o → ( 𝑔 ‘ 𝑘 ) ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) ) → ( 𝑔 ‘ 𝑘 ) ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) ) )
142		iffalse	⊢ ( ¬ ∪ ( 𝐹 ‘ 𝑘 ) ≈ 1_o → if ( ∪ ( 𝐹 ‘ 𝑘 ) ≈ 1_o , ∪ ∪ ( 𝐹 ‘ 𝑘 ) , ( 𝑔 ‘ 𝑘 ) ) = ( 𝑔 ‘ 𝑘 ) )
143	142	eleq1d	⊢ ( ¬ ∪ ( 𝐹 ‘ 𝑘 ) ≈ 1_o → ( if ( ∪ ( 𝐹 ‘ 𝑘 ) ≈ 1_o , ∪ ∪ ( 𝐹 ‘ 𝑘 ) , ( 𝑔 ‘ 𝑘 ) ) ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) ↔ ( 𝑔 ‘ 𝑘 ) ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) ) )
144	141 143	sylibrd	⊢ ( ¬ ∪ ( 𝐹 ‘ 𝑘 ) ≈ 1_o → ( ( ¬ ∪ ( 𝐹 ‘ 𝑘 ) ≈ 1_o → ( 𝑔 ‘ 𝑘 ) ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) ) → if ( ∪ ( 𝐹 ‘ 𝑘 ) ≈ 1_o , ∪ ∪ ( 𝐹 ‘ 𝑘 ) , ( 𝑔 ‘ 𝑘 ) ) ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) ) )
145	140 144	pm2.61d1	⊢ ( ( ( 𝜑 ∧ 𝑔 : { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1_o } ⟶ V ) ∧ 𝑘 ∈ 𝐴 ) → ( ( ¬ ∪ ( 𝐹 ‘ 𝑘 ) ≈ 1_o → ( 𝑔 ‘ 𝑘 ) ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) ) → if ( ∪ ( 𝐹 ‘ 𝑘 ) ≈ 1_o , ∪ ∪ ( 𝐹 ‘ 𝑘 ) , ( 𝑔 ‘ 𝑘 ) ) ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) ) )
146	145	ralimdva	⊢ ( ( 𝜑 ∧ 𝑔 : { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1_o } ⟶ V ) → ( ∀ 𝑘 ∈ 𝐴 ( ¬ ∪ ( 𝐹 ‘ 𝑘 ) ≈ 1_o → ( 𝑔 ‘ 𝑘 ) ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) ) → ∀ 𝑘 ∈ 𝐴 if ( ∪ ( 𝐹 ‘ 𝑘 ) ≈ 1_o , ∪ ∪ ( 𝐹 ‘ 𝑘 ) , ( 𝑔 ‘ 𝑘 ) ) ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) ) )
147	123 146	syl5bi	⊢ ( ( 𝜑 ∧ 𝑔 : { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1_o } ⟶ V ) → ( ∀ 𝑘 ∈ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1_o } ( 𝑔 ‘ 𝑘 ) ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) → ∀ 𝑘 ∈ 𝐴 if ( ∪ ( 𝐹 ‘ 𝑘 ) ≈ 1_o , ∪ ∪ ( 𝐹 ‘ 𝑘 ) , ( 𝑔 ‘ 𝑘 ) ) ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) ) )
148	147	impr	⊢ ( ( 𝜑 ∧ ( 𝑔 : { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1_o } ⟶ V ∧ ∀ 𝑘 ∈ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1_o } ( 𝑔 ‘ 𝑘 ) ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) ) ) → ∀ 𝑘 ∈ 𝐴 if ( ∪ ( 𝐹 ‘ 𝑘 ) ≈ 1_o , ∪ ∪ ( 𝐹 ‘ 𝑘 ) , ( 𝑔 ‘ 𝑘 ) ) ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) )
149		fneq1	⊢ ( 𝑓 = ( 𝑚 ∈ 𝐴 ↦ if ( ∪ ( 𝐹 ‘ 𝑚 ) ≈ 1_o , ∪ ∪ ( 𝐹 ‘ 𝑚 ) , ( 𝑔 ‘ 𝑚 ) ) ) → ( 𝑓 Fn 𝐴 ↔ ( 𝑚 ∈ 𝐴 ↦ if ( ∪ ( 𝐹 ‘ 𝑚 ) ≈ 1_o , ∪ ∪ ( 𝐹 ‘ 𝑚 ) , ( 𝑔 ‘ 𝑚 ) ) ) Fn 𝐴 ) )
150		fveq1	⊢ ( 𝑓 = ( 𝑚 ∈ 𝐴 ↦ if ( ∪ ( 𝐹 ‘ 𝑚 ) ≈ 1_o , ∪ ∪ ( 𝐹 ‘ 𝑚 ) , ( 𝑔 ‘ 𝑚 ) ) ) → ( 𝑓 ‘ 𝑘 ) = ( ( 𝑚 ∈ 𝐴 ↦ if ( ∪ ( 𝐹 ‘ 𝑚 ) ≈ 1_o , ∪ ∪ ( 𝐹 ‘ 𝑚 ) , ( 𝑔 ‘ 𝑚 ) ) ) ‘ 𝑘 ) )
151		fveq2	⊢ ( 𝑚 = 𝑘 → ( 𝐹 ‘ 𝑚 ) = ( 𝐹 ‘ 𝑘 ) )
152	151	unieqd	⊢ ( 𝑚 = 𝑘 → ∪ ( 𝐹 ‘ 𝑚 ) = ∪ ( 𝐹 ‘ 𝑘 ) )
153	152	breq1d	⊢ ( 𝑚 = 𝑘 → ( ∪ ( 𝐹 ‘ 𝑚 ) ≈ 1_o ↔ ∪ ( 𝐹 ‘ 𝑘 ) ≈ 1_o ) )
154	152	unieqd	⊢ ( 𝑚 = 𝑘 → ∪ ∪ ( 𝐹 ‘ 𝑚 ) = ∪ ∪ ( 𝐹 ‘ 𝑘 ) )
155		fveq2	⊢ ( 𝑚 = 𝑘 → ( 𝑔 ‘ 𝑚 ) = ( 𝑔 ‘ 𝑘 ) )
156	153 154 155	ifbieq12d	⊢ ( 𝑚 = 𝑘 → if ( ∪ ( 𝐹 ‘ 𝑚 ) ≈ 1_o , ∪ ∪ ( 𝐹 ‘ 𝑚 ) , ( 𝑔 ‘ 𝑚 ) ) = if ( ∪ ( 𝐹 ‘ 𝑘 ) ≈ 1_o , ∪ ∪ ( 𝐹 ‘ 𝑘 ) , ( 𝑔 ‘ 𝑘 ) ) )
157		fvex	⊢ ( 𝐹 ‘ 𝑘 ) ∈ V
158	157	uniex	⊢ ∪ ( 𝐹 ‘ 𝑘 ) ∈ V
159	158	uniex	⊢ ∪ ∪ ( 𝐹 ‘ 𝑘 ) ∈ V
160		fvex	⊢ ( 𝑔 ‘ 𝑘 ) ∈ V
161	159 160	ifex	⊢ if ( ∪ ( 𝐹 ‘ 𝑘 ) ≈ 1_o , ∪ ∪ ( 𝐹 ‘ 𝑘 ) , ( 𝑔 ‘ 𝑘 ) ) ∈ V
162	156 118 161	fvmpt	⊢ ( 𝑘 ∈ 𝐴 → ( ( 𝑚 ∈ 𝐴 ↦ if ( ∪ ( 𝐹 ‘ 𝑚 ) ≈ 1_o , ∪ ∪ ( 𝐹 ‘ 𝑚 ) , ( 𝑔 ‘ 𝑚 ) ) ) ‘ 𝑘 ) = if ( ∪ ( 𝐹 ‘ 𝑘 ) ≈ 1_o , ∪ ∪ ( 𝐹 ‘ 𝑘 ) , ( 𝑔 ‘ 𝑘 ) ) )
163	150 162	sylan9eq	⊢ ( ( 𝑓 = ( 𝑚 ∈ 𝐴 ↦ if ( ∪ ( 𝐹 ‘ 𝑚 ) ≈ 1_o , ∪ ∪ ( 𝐹 ‘ 𝑚 ) , ( 𝑔 ‘ 𝑚 ) ) ) ∧ 𝑘 ∈ 𝐴 ) → ( 𝑓 ‘ 𝑘 ) = if ( ∪ ( 𝐹 ‘ 𝑘 ) ≈ 1_o , ∪ ∪ ( 𝐹 ‘ 𝑘 ) , ( 𝑔 ‘ 𝑘 ) ) )
164	163	eleq1d	⊢ ( ( 𝑓 = ( 𝑚 ∈ 𝐴 ↦ if ( ∪ ( 𝐹 ‘ 𝑚 ) ≈ 1_o , ∪ ∪ ( 𝐹 ‘ 𝑚 ) , ( 𝑔 ‘ 𝑚 ) ) ) ∧ 𝑘 ∈ 𝐴 ) → ( ( 𝑓 ‘ 𝑘 ) ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) ↔ if ( ∪ ( 𝐹 ‘ 𝑘 ) ≈ 1_o , ∪ ∪ ( 𝐹 ‘ 𝑘 ) , ( 𝑔 ‘ 𝑘 ) ) ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) ) )
165	164	ralbidva	⊢ ( 𝑓 = ( 𝑚 ∈ 𝐴 ↦ if ( ∪ ( 𝐹 ‘ 𝑚 ) ≈ 1_o , ∪ ∪ ( 𝐹 ‘ 𝑚 ) , ( 𝑔 ‘ 𝑚 ) ) ) → ( ∀ 𝑘 ∈ 𝐴 ( 𝑓 ‘ 𝑘 ) ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) ↔ ∀ 𝑘 ∈ 𝐴 if ( ∪ ( 𝐹 ‘ 𝑘 ) ≈ 1_o , ∪ ∪ ( 𝐹 ‘ 𝑘 ) , ( 𝑔 ‘ 𝑘 ) ) ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) ) )
166	149 165	anbi12d	⊢ ( 𝑓 = ( 𝑚 ∈ 𝐴 ↦ if ( ∪ ( 𝐹 ‘ 𝑚 ) ≈ 1_o , ∪ ∪ ( 𝐹 ‘ 𝑚 ) , ( 𝑔 ‘ 𝑚 ) ) ) → ( ( 𝑓 Fn 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑓 ‘ 𝑘 ) ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) ) ↔ ( ( 𝑚 ∈ 𝐴 ↦ if ( ∪ ( 𝐹 ‘ 𝑚 ) ≈ 1_o , ∪ ∪ ( 𝐹 ‘ 𝑚 ) , ( 𝑔 ‘ 𝑚 ) ) ) Fn 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 if ( ∪ ( 𝐹 ‘ 𝑘 ) ≈ 1_o , ∪ ∪ ( 𝐹 ‘ 𝑘 ) , ( 𝑔 ‘ 𝑘 ) ) ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) ) ) )
167	166	spcegv	⊢ ( ( 𝑚 ∈ 𝐴 ↦ if ( ∪ ( 𝐹 ‘ 𝑚 ) ≈ 1_o , ∪ ∪ ( 𝐹 ‘ 𝑚 ) , ( 𝑔 ‘ 𝑚 ) ) ) ∈ V → ( ( ( 𝑚 ∈ 𝐴 ↦ if ( ∪ ( 𝐹 ‘ 𝑚 ) ≈ 1_o , ∪ ∪ ( 𝐹 ‘ 𝑚 ) , ( 𝑔 ‘ 𝑚 ) ) ) Fn 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 if ( ∪ ( 𝐹 ‘ 𝑘 ) ≈ 1_o , ∪ ∪ ( 𝐹 ‘ 𝑘 ) , ( 𝑔 ‘ 𝑘 ) ) ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) ) → ∃ 𝑓 ( 𝑓 Fn 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑓 ‘ 𝑘 ) ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) ) ) )
168	167	3impib	⊢ ( ( ( 𝑚 ∈ 𝐴 ↦ if ( ∪ ( 𝐹 ‘ 𝑚 ) ≈ 1_o , ∪ ∪ ( 𝐹 ‘ 𝑚 ) , ( 𝑔 ‘ 𝑚 ) ) ) ∈ V ∧ ( 𝑚 ∈ 𝐴 ↦ if ( ∪ ( 𝐹 ‘ 𝑚 ) ≈ 1_o , ∪ ∪ ( 𝐹 ‘ 𝑚 ) , ( 𝑔 ‘ 𝑚 ) ) ) Fn 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 if ( ∪ ( 𝐹 ‘ 𝑘 ) ≈ 1_o , ∪ ∪ ( 𝐹 ‘ 𝑘 ) , ( 𝑔 ‘ 𝑘 ) ) ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) ) → ∃ 𝑓 ( 𝑓 Fn 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑓 ‘ 𝑘 ) ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) ) )
169	111 120 148 168	syl3anc	⊢ ( ( 𝜑 ∧ ( 𝑔 : { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1_o } ⟶ V ∧ ∀ 𝑘 ∈ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1_o } ( 𝑔 ‘ 𝑘 ) ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) ) ) → ∃ 𝑓 ( 𝑓 Fn 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑓 ‘ 𝑘 ) ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) ) )
170	109 169	exlimddv	⊢ ( 𝜑 → ∃ 𝑓 ( 𝑓 Fn 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑓 ‘ 𝑘 ) ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) ) )

Metamath Proof Explorer

Theorem ptcmplem3

Proof