Metamath Proof Explorer

Theorem kelac1

Description: Kelley's choice, basic form: if a collection of sets can be cast as closed sets in the factors of a topology, and there is a definable element in each topology (which need not be in the closed set - if it were this would be trivial), then compactness (via finite intersection) guarantees that the final product is nonempty. (Contributed by Stefan O'Rear, 22-Feb-2015)

Ref Expression
Hypotheses kelac1.z ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝑆 ≠ ∅ )
kelac1.j ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝐽 ∈ Top )
kelac1.c ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝐶 ∈ ( Clsd ‘ 𝐽 ) )
kelac1.b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝐵 : 𝑆 –1-1-onto→ 𝐶 )
kelac1.u ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝑈 ∈ ∪ 𝐽 )
kelac1.k ⊢ ( 𝜑 → ( ∏t ‘ ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) ) ∈ Comp )
Assertion kelac1 ( 𝜑 → X 𝑥 ∈ 𝐼 𝑆 ≠ ∅ )

Proof

Step Hyp Ref Expression
1 kelac1.z ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝑆 ≠ ∅ )
2 kelac1.j ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝐽 ∈ Top )
3 kelac1.c ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝐶 ∈ ( Clsd ‘ 𝐽 ) )
4 kelac1.b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝐵 : 𝑆 –1-1-onto→ 𝐶 )
5 kelac1.u ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝑈 ∈ ∪ 𝐽 )
6 kelac1.k ⊢ ( 𝜑 → ( ∏t ‘ ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) ) ∈ Comp )
7 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
8 7 cldss ⊢ ( 𝐶 ∈ ( Clsd ‘ 𝐽 ) → 𝐶 ⊆ ∪ 𝐽 )
9 3 8 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝐶 ⊆ ∪ 𝐽 )
10 9 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐼 𝐶 ⊆ ∪ 𝐽 )
11 boxriin ⊢ ( ∀ 𝑥 ∈ 𝐼 𝐶 ⊆ ∪ 𝐽 → X 𝑥 ∈ 𝐼 𝐶 = ( X 𝑥 ∈ 𝐼 ∪ 𝐽 ∩ ∩ 𝑦 ∈ 𝐼 X 𝑥 ∈ 𝐼 if ( 𝑥 = 𝑦 , 𝐶 , ∪ 𝐽 ) ) )
12 10 11 syl ⊢ ( 𝜑 → X 𝑥 ∈ 𝐼 𝐶 = ( X 𝑥 ∈ 𝐼 ∪ 𝐽 ∩ ∩ 𝑦 ∈ 𝐼 X 𝑥 ∈ 𝐼 if ( 𝑥 = 𝑦 , 𝐶 , ∪ 𝐽 ) ) )
13 cmptop ⊢ ( ( ∏t ‘ ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) ) ∈ Comp → ( ∏t ‘ ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) ) ∈ Top )
14 0ntop ⊢ ¬ ∅ ∈ Top
15 fvprc ⊢ ( ¬ ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) ∈ V → ( ∏t ‘ ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) ) = ∅ )
16 15 eleq1d ⊢ ( ¬ ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) ∈ V → ( ( ∏t ‘ ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) ) ∈ Top ↔ ∅ ∈ Top ) )
17 14 16 mtbiri ⊢ ( ¬ ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) ∈ V → ¬ ( ∏t ‘ ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) ) ∈ Top )
18 17 con4i ⊢ ( ( ∏t ‘ ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) ) ∈ Top → ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) ∈ V )
19 6 13 18 3syl ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) ∈ V )
20 2 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) : 𝐼 ⟶ Top )
21 dmfex ⊢ ( ( ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) ∈ V ∧ ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) : 𝐼 ⟶ Top ) → 𝐼 ∈ V )
22 19 20 21 syl2anc ⊢ ( 𝜑 → 𝐼 ∈ V )
23 2 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐼 𝐽 ∈ Top )
24 eqid ⊢ ( ∏t ‘ ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) ) = ( ∏t ‘ ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) )
25 24 ptunimpt ⊢ ( ( 𝐼 ∈ V ∧ ∀ 𝑥 ∈ 𝐼 𝐽 ∈ Top ) → X 𝑥 ∈ 𝐼 ∪ 𝐽 = ∪ ( ∏t ‘ ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) ) )
26 22 23 25 syl2anc ⊢ ( 𝜑 → X 𝑥 ∈ 𝐼 ∪ 𝐽 = ∪ ( ∏t ‘ ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) ) )
27 26 ineq1d ⊢ ( 𝜑 → ( X 𝑥 ∈ 𝐼 ∪ 𝐽 ∩ ∩ 𝑦 ∈ 𝐼 X 𝑥 ∈ 𝐼 if ( 𝑥 = 𝑦 , 𝐶 , ∪ 𝐽 ) ) = ( ∪ ( ∏t ‘ ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) ) ∩ ∩ 𝑦 ∈ 𝐼 X 𝑥 ∈ 𝐼 if ( 𝑥 = 𝑦 , 𝐶 , ∪ 𝐽 ) ) )
28 eqid ⊢ ∪ ( ∏t ‘ ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) ) = ∪ ( ∏t ‘ ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) )
29 7 topcld ⊢ ( 𝐽 ∈ Top → ∪ 𝐽 ∈ ( Clsd ‘ 𝐽 ) )
30 2 29 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ∪ 𝐽 ∈ ( Clsd ‘ 𝐽 ) )
31 3 30 ifcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → if ( 𝑥 = 𝑦 , 𝐶 , ∪ 𝐽 ) ∈ ( Clsd ‘ 𝐽 ) )
32 22 2 31 ptcldmpt ⊢ ( 𝜑 → X 𝑥 ∈ 𝐼 if ( 𝑥 = 𝑦 , 𝐶 , ∪ 𝐽 ) ∈ ( Clsd ‘ ( ∏t ‘ ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) ) ) )
33 32 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐼 ) → X 𝑥 ∈ 𝐼 if ( 𝑥 = 𝑦 , 𝐶 , ∪ 𝐽 ) ∈ ( Clsd ‘ ( ∏t ‘ ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) ) ) )
34 simprr ⊢ ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin ) ) → 𝑧 ∈ Fin )
35 f1ofo ⊢ ( 𝐵 : 𝑆 –1-1-onto→ 𝐶 → 𝐵 : 𝑆 –onto→ 𝐶 )
36 foima ⊢ ( 𝐵 : 𝑆 –onto→ 𝐶 → ( 𝐵 “ 𝑆 ) = 𝐶 )
37 4 35 36 3syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝐵 “ 𝑆 ) = 𝐶 )
38 37 eqcomd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝐶 = ( 𝐵 “ 𝑆 ) )
39 f1ofn ⊢ ( 𝐵 : 𝑆 –1-1-onto→ 𝐶 → 𝐵 Fn 𝑆 )
40 4 39 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝐵 Fn 𝑆 )
41 ssid ⊢ 𝑆 ⊆ 𝑆
42 fnimaeq0 ⊢ ( ( 𝐵 Fn 𝑆 ∧ 𝑆 ⊆ 𝑆 ) → ( ( 𝐵 “ 𝑆 ) = ∅ ↔ 𝑆 = ∅ ) )
43 40 41 42 sylancl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝐵 “ 𝑆 ) = ∅ ↔ 𝑆 = ∅ ) )
44 43 necon3bid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝐵 “ 𝑆 ) ≠ ∅ ↔ 𝑆 ≠ ∅ ) )
45 1 44 mpbird ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝐵 “ 𝑆 ) ≠ ∅ )
46 38 45 eqnetrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝐶 ≠ ∅ )
47 n0 ⊢ ( 𝐶 ≠ ∅ ↔ ∃ 𝑤 𝑤 ∈ 𝐶 )
48 46 47 sylib ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ∃ 𝑤 𝑤 ∈ 𝐶 )
49 rexv ⊢ ( ∃ 𝑤 ∈ V 𝑤 ∈ 𝐶 ↔ ∃ 𝑤 𝑤 ∈ 𝐶 )
50 48 49 sylibr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ∃ 𝑤 ∈ V 𝑤 ∈ 𝐶 )
51 50 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐼 ∃ 𝑤 ∈ V 𝑤 ∈ 𝐶 )
52 ssralv ⊢ ( 𝑧 ⊆ 𝐼 → ( ∀ 𝑥 ∈ 𝐼 ∃ 𝑤 ∈ V 𝑤 ∈ 𝐶 → ∀ 𝑥 ∈ 𝑧 ∃ 𝑤 ∈ V 𝑤 ∈ 𝐶 ) )
53 52 adantr ⊢ ( ( 𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin ) → ( ∀ 𝑥 ∈ 𝐼 ∃ 𝑤 ∈ V 𝑤 ∈ 𝐶 → ∀ 𝑥 ∈ 𝑧 ∃ 𝑤 ∈ V 𝑤 ∈ 𝐶 ) )
54 51 53 mpan9 ⊢ ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin ) ) → ∀ 𝑥 ∈ 𝑧 ∃ 𝑤 ∈ V 𝑤 ∈ 𝐶 )
55 eleq1 ⊢ ( 𝑤 = ( 𝑓 ‘ 𝑥 ) → ( 𝑤 ∈ 𝐶 ↔ ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) )
56 55 ac6sfi ⊢ ( ( 𝑧 ∈ Fin ∧ ∀ 𝑥 ∈ 𝑧 ∃ 𝑤 ∈ V 𝑤 ∈ 𝐶 ) → ∃ 𝑓 ( 𝑓 : 𝑧 ⟶ V ∧ ∀ 𝑥 ∈ 𝑧 ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) )
57 34 54 56 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin ) ) → ∃ 𝑓 ( 𝑓 : 𝑧 ⟶ V ∧ ∀ 𝑥 ∈ 𝑧 ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) )
58 26 eqcomd ⊢ ( 𝜑 → ∪ ( ∏t ‘ ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) ) = X 𝑥 ∈ 𝐼 ∪ 𝐽 )
59 58 ineq1d ⊢ ( 𝜑 → ( ∪ ( ∏t ‘ ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) ) ∩ ∩ 𝑦 ∈ 𝑧 X 𝑥 ∈ 𝐼 if ( 𝑥 = 𝑦 , 𝐶 , ∪ 𝐽 ) ) = ( X 𝑥 ∈ 𝐼 ∪ 𝐽 ∩ ∩ 𝑦 ∈ 𝑧 X 𝑥 ∈ 𝐼 if ( 𝑥 = 𝑦 , 𝐶 , ∪ 𝐽 ) ) )
60 59 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin ) ) ∧ ∀ 𝑥 ∈ 𝑧 ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) → ( ∪ ( ∏t ‘ ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) ) ∩ ∩ 𝑦 ∈ 𝑧 X 𝑥 ∈ 𝐼 if ( 𝑥 = 𝑦 , 𝐶 , ∪ 𝐽 ) ) = ( X 𝑥 ∈ 𝐼 ∪ 𝐽 ∩ ∩ 𝑦 ∈ 𝑧 X 𝑥 ∈ 𝐼 if ( 𝑥 = 𝑦 , 𝐶 , ∪ 𝐽 ) ) )
61 iftrue ⊢ ( 𝑥 ∈ 𝑧 → if ( 𝑥 ∈ 𝑧 , ( 𝑓 ‘ 𝑥 ) , 𝑈 ) = ( 𝑓 ‘ 𝑥 ) )
62 61 ad2antrl ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin ) ) ∧ ( 𝑥 ∈ 𝑧 ∧ ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) ) → if ( 𝑥 ∈ 𝑧 , ( 𝑓 ‘ 𝑥 ) , 𝑈 ) = ( 𝑓 ‘ 𝑥 ) )
63 simpll ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin ) ) ∧ 𝑥 ∈ 𝑧 ) → 𝜑 )
64 simprl ⊢ ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin ) ) → 𝑧 ⊆ 𝐼 )
65 64 sselda ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin ) ) ∧ 𝑥 ∈ 𝑧 ) → 𝑥 ∈ 𝐼 )
66 63 65 9 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin ) ) ∧ 𝑥 ∈ 𝑧 ) → 𝐶 ⊆ ∪ 𝐽 )
67 66 sseld ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin ) ) ∧ 𝑥 ∈ 𝑧 ) → ( ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 → ( 𝑓 ‘ 𝑥 ) ∈ ∪ 𝐽 ) )
68 67 impr ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin ) ) ∧ ( 𝑥 ∈ 𝑧 ∧ ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) ) → ( 𝑓 ‘ 𝑥 ) ∈ ∪ 𝐽 )
69 62 68 eqeltrd ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin ) ) ∧ ( 𝑥 ∈ 𝑧 ∧ ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) ) → if ( 𝑥 ∈ 𝑧 , ( 𝑓 ‘ 𝑥 ) , 𝑈 ) ∈ ∪ 𝐽 )
70 69 expr ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin ) ) ∧ 𝑥 ∈ 𝑧 ) → ( ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 → if ( 𝑥 ∈ 𝑧 , ( 𝑓 ‘ 𝑥 ) , 𝑈 ) ∈ ∪ 𝐽 ) )
71 70 ralimdva ⊢ ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin ) ) → ( ∀ 𝑥 ∈ 𝑧 ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 → ∀ 𝑥 ∈ 𝑧 if ( 𝑥 ∈ 𝑧 , ( 𝑓 ‘ 𝑥 ) , 𝑈 ) ∈ ∪ 𝐽 ) )
72 71 imp ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin ) ) ∧ ∀ 𝑥 ∈ 𝑧 ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) → ∀ 𝑥 ∈ 𝑧 if ( 𝑥 ∈ 𝑧 , ( 𝑓 ‘ 𝑥 ) , 𝑈 ) ∈ ∪ 𝐽 )
73 eldifn ⊢ ( 𝑥 ∈ ( 𝐼 ∖ 𝑧 ) → ¬ 𝑥 ∈ 𝑧 )
74 73 iffalsed ⊢ ( 𝑥 ∈ ( 𝐼 ∖ 𝑧 ) → if ( 𝑥 ∈ 𝑧 , ( 𝑓 ‘ 𝑥 ) , 𝑈 ) = 𝑈 )
75 74 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∖ 𝑧 ) ) → if ( 𝑥 ∈ 𝑧 , ( 𝑓 ‘ 𝑥 ) , 𝑈 ) = 𝑈 )
76 eldifi ⊢ ( 𝑥 ∈ ( 𝐼 ∖ 𝑧 ) → 𝑥 ∈ 𝐼 )
77 76 5 sylan2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∖ 𝑧 ) ) → 𝑈 ∈ ∪ 𝐽 )
78 75 77 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∖ 𝑧 ) ) → if ( 𝑥 ∈ 𝑧 , ( 𝑓 ‘ 𝑥 ) , 𝑈 ) ∈ ∪ 𝐽 )
79 78 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 𝐼 ∖ 𝑧 ) if ( 𝑥 ∈ 𝑧 , ( 𝑓 ‘ 𝑥 ) , 𝑈 ) ∈ ∪ 𝐽 )
80 79 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin ) ) ∧ ∀ 𝑥 ∈ 𝑧 ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) → ∀ 𝑥 ∈ ( 𝐼 ∖ 𝑧 ) if ( 𝑥 ∈ 𝑧 , ( 𝑓 ‘ 𝑥 ) , 𝑈 ) ∈ ∪ 𝐽 )
81 ralun ⊢ ( ( ∀ 𝑥 ∈ 𝑧 if ( 𝑥 ∈ 𝑧 , ( 𝑓 ‘ 𝑥 ) , 𝑈 ) ∈ ∪ 𝐽 ∧ ∀ 𝑥 ∈ ( 𝐼 ∖ 𝑧 ) if ( 𝑥 ∈ 𝑧 , ( 𝑓 ‘ 𝑥 ) , 𝑈 ) ∈ ∪ 𝐽 ) → ∀ 𝑥 ∈ ( 𝑧 ∪ ( 𝐼 ∖ 𝑧 ) ) if ( 𝑥 ∈ 𝑧 , ( 𝑓 ‘ 𝑥 ) , 𝑈 ) ∈ ∪ 𝐽 )
82 72 80 81 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin ) ) ∧ ∀ 𝑥 ∈ 𝑧 ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) → ∀ 𝑥 ∈ ( 𝑧 ∪ ( 𝐼 ∖ 𝑧 ) ) if ( 𝑥 ∈ 𝑧 , ( 𝑓 ‘ 𝑥 ) , 𝑈 ) ∈ ∪ 𝐽 )
83 undif ⊢ ( 𝑧 ⊆ 𝐼 ↔ ( 𝑧 ∪ ( 𝐼 ∖ 𝑧 ) ) = 𝐼 )
84 83 biimpi ⊢ ( 𝑧 ⊆ 𝐼 → ( 𝑧 ∪ ( 𝐼 ∖ 𝑧 ) ) = 𝐼 )
85 84 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin ) ) → ( 𝑧 ∪ ( 𝐼 ∖ 𝑧 ) ) = 𝐼 )
86 85 raleqdv ⊢ ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin ) ) → ( ∀ 𝑥 ∈ ( 𝑧 ∪ ( 𝐼 ∖ 𝑧 ) ) if ( 𝑥 ∈ 𝑧 , ( 𝑓 ‘ 𝑥 ) , 𝑈 ) ∈ ∪ 𝐽 ↔ ∀ 𝑥 ∈ 𝐼 if ( 𝑥 ∈ 𝑧 , ( 𝑓 ‘ 𝑥 ) , 𝑈 ) ∈ ∪ 𝐽 ) )
87 86 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin ) ) ∧ ∀ 𝑥 ∈ 𝑧 ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) → ( ∀ 𝑥 ∈ ( 𝑧 ∪ ( 𝐼 ∖ 𝑧 ) ) if ( 𝑥 ∈ 𝑧 , ( 𝑓 ‘ 𝑥 ) , 𝑈 ) ∈ ∪ 𝐽 ↔ ∀ 𝑥 ∈ 𝐼 if ( 𝑥 ∈ 𝑧 , ( 𝑓 ‘ 𝑥 ) , 𝑈 ) ∈ ∪ 𝐽 ) )
88 82 87 mpbid ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin ) ) ∧ ∀ 𝑥 ∈ 𝑧 ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) → ∀ 𝑥 ∈ 𝐼 if ( 𝑥 ∈ 𝑧 , ( 𝑓 ‘ 𝑥 ) , 𝑈 ) ∈ ∪ 𝐽 )
89 22 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin ) ) ∧ ∀ 𝑥 ∈ 𝑧 ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) → 𝐼 ∈ V )
90 mptelixpg ⊢ ( 𝐼 ∈ V → ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝑧 , ( 𝑓 ‘ 𝑥 ) , 𝑈 ) ) ∈ X 𝑥 ∈ 𝐼 ∪ 𝐽 ↔ ∀ 𝑥 ∈ 𝐼 if ( 𝑥 ∈ 𝑧 , ( 𝑓 ‘ 𝑥 ) , 𝑈 ) ∈ ∪ 𝐽 ) )
91 89 90 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin ) ) ∧ ∀ 𝑥 ∈ 𝑧 ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) → ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝑧 , ( 𝑓 ‘ 𝑥 ) , 𝑈 ) ) ∈ X 𝑥 ∈ 𝐼 ∪ 𝐽 ↔ ∀ 𝑥 ∈ 𝐼 if ( 𝑥 ∈ 𝑧 , ( 𝑓 ‘ 𝑥 ) , 𝑈 ) ∈ ∪ 𝐽 ) )
92 88 91 mpbird ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin ) ) ∧ ∀ 𝑥 ∈ 𝑧 ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) → ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝑧 , ( 𝑓 ‘ 𝑥 ) , 𝑈 ) ) ∈ X 𝑥 ∈ 𝐼 ∪ 𝐽 )
93 eleq2 ⊢ ( 𝐶 = if ( 𝑥 = 𝑦 , 𝐶 , ∪ 𝐽 ) → ( ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ↔ ( 𝑓 ‘ 𝑥 ) ∈ if ( 𝑥 = 𝑦 , 𝐶 , ∪ 𝐽 ) ) )
94 eleq2 ⊢ ( ∪ 𝐽 = if ( 𝑥 = 𝑦 , 𝐶 , ∪ 𝐽 ) → ( ( 𝑓 ‘ 𝑥 ) ∈ ∪ 𝐽 ↔ ( 𝑓 ‘ 𝑥 ) ∈ if ( 𝑥 = 𝑦 , 𝐶 , ∪ 𝐽 ) ) )
95 simplrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin ) ) ∧ ( 𝑥 ∈ 𝑧 ∧ ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) ) ∧ 𝑥 = 𝑦 ) → ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 )
96 68 adantr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin ) ) ∧ ( 𝑥 ∈ 𝑧 ∧ ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) ) ∧ ¬ 𝑥 = 𝑦 ) → ( 𝑓 ‘ 𝑥 ) ∈ ∪ 𝐽 )
97 93 94 95 96 ifbothda ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin ) ) ∧ ( 𝑥 ∈ 𝑧 ∧ ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) ) → ( 𝑓 ‘ 𝑥 ) ∈ if ( 𝑥 = 𝑦 , 𝐶 , ∪ 𝐽 ) )
98 62 97 eqeltrd ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin ) ) ∧ ( 𝑥 ∈ 𝑧 ∧ ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) ) → if ( 𝑥 ∈ 𝑧 , ( 𝑓 ‘ 𝑥 ) , 𝑈 ) ∈ if ( 𝑥 = 𝑦 , 𝐶 , ∪ 𝐽 ) )
99 98 expr ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin ) ) ∧ 𝑥 ∈ 𝑧 ) → ( ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 → if ( 𝑥 ∈ 𝑧 , ( 𝑓 ‘ 𝑥 ) , 𝑈 ) ∈ if ( 𝑥 = 𝑦 , 𝐶 , ∪ 𝐽 ) ) )
100 99 ralimdva ⊢ ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin ) ) → ( ∀ 𝑥 ∈ 𝑧 ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 → ∀ 𝑥 ∈ 𝑧 if ( 𝑥 ∈ 𝑧 , ( 𝑓 ‘ 𝑥 ) , 𝑈 ) ∈ if ( 𝑥 = 𝑦 , 𝐶 , ∪ 𝐽 ) ) )
101 100 imp ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin ) ) ∧ ∀ 𝑥 ∈ 𝑧 ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) → ∀ 𝑥 ∈ 𝑧 if ( 𝑥 ∈ 𝑧 , ( 𝑓 ‘ 𝑥 ) , 𝑈 ) ∈ if ( 𝑥 = 𝑦 , 𝐶 , ∪ 𝐽 ) )
102 101 adantr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin ) ) ∧ ∀ 𝑥 ∈ 𝑧 ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) ∧ 𝑦 ∈ 𝑧 ) → ∀ 𝑥 ∈ 𝑧 if ( 𝑥 ∈ 𝑧 , ( 𝑓 ‘ 𝑥 ) , 𝑈 ) ∈ if ( 𝑥 = 𝑦 , 𝐶 , ∪ 𝐽 ) )
103 77 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑧 ) ∧ 𝑥 ∈ ( 𝐼 ∖ 𝑧 ) ) → 𝑈 ∈ ∪ 𝐽 )
104 74 adantl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑧 ) ∧ 𝑥 ∈ ( 𝐼 ∖ 𝑧 ) ) → if ( 𝑥 ∈ 𝑧 , ( 𝑓 ‘ 𝑥 ) , 𝑈 ) = 𝑈 )
105 disjdifr ⊢ ( ( 𝐼 ∖ 𝑧 ) ∩ 𝑧 ) = ∅
106 105 a1i ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑧 ) ∧ 𝑥 ∈ ( 𝐼 ∖ 𝑧 ) ) → ( ( 𝐼 ∖ 𝑧 ) ∩ 𝑧 ) = ∅ )
107 simpr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑧 ) ∧ 𝑥 ∈ ( 𝐼 ∖ 𝑧 ) ) → 𝑥 ∈ ( 𝐼 ∖ 𝑧 ) )
108 simplr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑧 ) ∧ 𝑥 ∈ ( 𝐼 ∖ 𝑧 ) ) → 𝑦 ∈ 𝑧 )
109 disjne ⊢ ( ( ( ( 𝐼 ∖ 𝑧 ) ∩ 𝑧 ) = ∅ ∧ 𝑥 ∈ ( 𝐼 ∖ 𝑧 ) ∧ 𝑦 ∈ 𝑧 ) → 𝑥 ≠ 𝑦 )
110 106 107 108 109 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑧 ) ∧ 𝑥 ∈ ( 𝐼 ∖ 𝑧 ) ) → 𝑥 ≠ 𝑦 )
111 110 neneqd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑧 ) ∧ 𝑥 ∈ ( 𝐼 ∖ 𝑧 ) ) → ¬ 𝑥 = 𝑦 )
112 111 iffalsed ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑧 ) ∧ 𝑥 ∈ ( 𝐼 ∖ 𝑧 ) ) → if ( 𝑥 = 𝑦 , 𝐶 , ∪ 𝐽 ) = ∪ 𝐽 )
113 103 104 112 3eltr4d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑧 ) ∧ 𝑥 ∈ ( 𝐼 ∖ 𝑧 ) ) → if ( 𝑥 ∈ 𝑧 , ( 𝑓 ‘ 𝑥 ) , 𝑈 ) ∈ if ( 𝑥 = 𝑦 , 𝐶 , ∪ 𝐽 ) )
114 113 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑧 ) → ∀ 𝑥 ∈ ( 𝐼 ∖ 𝑧 ) if ( 𝑥 ∈ 𝑧 , ( 𝑓 ‘ 𝑥 ) , 𝑈 ) ∈ if ( 𝑥 = 𝑦 , 𝐶 , ∪ 𝐽 ) )
115 114 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin ) ) ∧ 𝑦 ∈ 𝑧 ) → ∀ 𝑥 ∈ ( 𝐼 ∖ 𝑧 ) if ( 𝑥 ∈ 𝑧 , ( 𝑓 ‘ 𝑥 ) , 𝑈 ) ∈ if ( 𝑥 = 𝑦 , 𝐶 , ∪ 𝐽 ) )
116 115 adantlr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin ) ) ∧ ∀ 𝑥 ∈ 𝑧 ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) ∧ 𝑦 ∈ 𝑧 ) → ∀ 𝑥 ∈ ( 𝐼 ∖ 𝑧 ) if ( 𝑥 ∈ 𝑧 , ( 𝑓 ‘ 𝑥 ) , 𝑈 ) ∈ if ( 𝑥 = 𝑦 , 𝐶 , ∪ 𝐽 ) )
117 ralun ⊢ ( ( ∀ 𝑥 ∈ 𝑧 if ( 𝑥 ∈ 𝑧 , ( 𝑓 ‘ 𝑥 ) , 𝑈 ) ∈ if ( 𝑥 = 𝑦 , 𝐶 , ∪ 𝐽 ) ∧ ∀ 𝑥 ∈ ( 𝐼 ∖ 𝑧 ) if ( 𝑥 ∈ 𝑧 , ( 𝑓 ‘ 𝑥 ) , 𝑈 ) ∈ if ( 𝑥 = 𝑦 , 𝐶 , ∪ 𝐽 ) ) → ∀ 𝑥 ∈ ( 𝑧 ∪ ( 𝐼 ∖ 𝑧 ) ) if ( 𝑥 ∈ 𝑧 , ( 𝑓 ‘ 𝑥 ) , 𝑈 ) ∈ if ( 𝑥 = 𝑦 , 𝐶 , ∪ 𝐽 ) )
118 102 116 117 syl2anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin ) ) ∧ ∀ 𝑥 ∈ 𝑧 ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) ∧ 𝑦 ∈ 𝑧 ) → ∀ 𝑥 ∈ ( 𝑧 ∪ ( 𝐼 ∖ 𝑧 ) ) if ( 𝑥 ∈ 𝑧 , ( 𝑓 ‘ 𝑥 ) , 𝑈 ) ∈ if ( 𝑥 = 𝑦 , 𝐶 , ∪ 𝐽 ) )
119 85 raleqdv ⊢ ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin ) ) → ( ∀ 𝑥 ∈ ( 𝑧 ∪ ( 𝐼 ∖ 𝑧 ) ) if ( 𝑥 ∈ 𝑧 , ( 𝑓 ‘ 𝑥 ) , 𝑈 ) ∈ if ( 𝑥 = 𝑦 , 𝐶 , ∪ 𝐽 ) ↔ ∀ 𝑥 ∈ 𝐼 if ( 𝑥 ∈ 𝑧 , ( 𝑓 ‘ 𝑥 ) , 𝑈 ) ∈ if ( 𝑥 = 𝑦 , 𝐶 , ∪ 𝐽 ) ) )
120 119 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin ) ) ∧ ∀ 𝑥 ∈ 𝑧 ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) ∧ 𝑦 ∈ 𝑧 ) → ( ∀ 𝑥 ∈ ( 𝑧 ∪ ( 𝐼 ∖ 𝑧 ) ) if ( 𝑥 ∈ 𝑧 , ( 𝑓 ‘ 𝑥 ) , 𝑈 ) ∈ if ( 𝑥 = 𝑦 , 𝐶 , ∪ 𝐽 ) ↔ ∀ 𝑥 ∈ 𝐼 if ( 𝑥 ∈ 𝑧 , ( 𝑓 ‘ 𝑥 ) , 𝑈 ) ∈ if ( 𝑥 = 𝑦 , 𝐶 , ∪ 𝐽 ) ) )
121 118 120 mpbid ⊢ ( ( ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin ) ) ∧ ∀ 𝑥 ∈ 𝑧 ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) ∧ 𝑦 ∈ 𝑧 ) → ∀ 𝑥 ∈ 𝐼 if ( 𝑥 ∈ 𝑧 , ( 𝑓 ‘ 𝑥 ) , 𝑈 ) ∈ if ( 𝑥 = 𝑦 , 𝐶 , ∪ 𝐽 ) )
122 22 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin ) ) ∧ ∀ 𝑥 ∈ 𝑧 ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) ∧ 𝑦 ∈ 𝑧 ) → 𝐼 ∈ V )
123 mptelixpg ⊢ ( 𝐼 ∈ V → ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝑧 , ( 𝑓 ‘ 𝑥 ) , 𝑈 ) ) ∈ X 𝑥 ∈ 𝐼 if ( 𝑥 = 𝑦 , 𝐶 , ∪ 𝐽 ) ↔ ∀ 𝑥 ∈ 𝐼 if ( 𝑥 ∈ 𝑧 , ( 𝑓 ‘ 𝑥 ) , 𝑈 ) ∈ if ( 𝑥 = 𝑦 , 𝐶 , ∪ 𝐽 ) ) )
124 122 123 syl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin ) ) ∧ ∀ 𝑥 ∈ 𝑧 ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) ∧ 𝑦 ∈ 𝑧 ) → ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝑧 , ( 𝑓 ‘ 𝑥 ) , 𝑈 ) ) ∈ X 𝑥 ∈ 𝐼 if ( 𝑥 = 𝑦 , 𝐶 , ∪ 𝐽 ) ↔ ∀ 𝑥 ∈ 𝐼 if ( 𝑥 ∈ 𝑧 , ( 𝑓 ‘ 𝑥 ) , 𝑈 ) ∈ if ( 𝑥 = 𝑦 , 𝐶 , ∪ 𝐽 ) ) )
125 121 124 mpbird ⊢ ( ( ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin ) ) ∧ ∀ 𝑥 ∈ 𝑧 ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) ∧ 𝑦 ∈ 𝑧 ) → ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝑧 , ( 𝑓 ‘ 𝑥 ) , 𝑈 ) ) ∈ X 𝑥 ∈ 𝐼 if ( 𝑥 = 𝑦 , 𝐶 , ∪ 𝐽 ) )
126 125 ralrimiva ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin ) ) ∧ ∀ 𝑥 ∈ 𝑧 ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) → ∀ 𝑦 ∈ 𝑧 ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝑧 , ( 𝑓 ‘ 𝑥 ) , 𝑈 ) ) ∈ X 𝑥 ∈ 𝐼 if ( 𝑥 = 𝑦 , 𝐶 , ∪ 𝐽 ) )
127 mptexg ⊢ ( 𝐼 ∈ V → ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝑧 , ( 𝑓 ‘ 𝑥 ) , 𝑈 ) ) ∈ V )
128 22 127 syl ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝑧 , ( 𝑓 ‘ 𝑥 ) , 𝑈 ) ) ∈ V )
129 128 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin ) ) ∧ ∀ 𝑥 ∈ 𝑧 ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) → ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝑧 , ( 𝑓 ‘ 𝑥 ) , 𝑈 ) ) ∈ V )
130 eliin ⊢ ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝑧 , ( 𝑓 ‘ 𝑥 ) , 𝑈 ) ) ∈ V → ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝑧 , ( 𝑓 ‘ 𝑥 ) , 𝑈 ) ) ∈ ∩ 𝑦 ∈ 𝑧 X 𝑥 ∈ 𝐼 if ( 𝑥 = 𝑦 , 𝐶 , ∪ 𝐽 ) ↔ ∀ 𝑦 ∈ 𝑧 ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝑧 , ( 𝑓 ‘ 𝑥 ) , 𝑈 ) ) ∈ X 𝑥 ∈ 𝐼 if ( 𝑥 = 𝑦 , 𝐶 , ∪ 𝐽 ) ) )
131 129 130 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin ) ) ∧ ∀ 𝑥 ∈ 𝑧 ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) → ( ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝑧 , ( 𝑓 ‘ 𝑥 ) , 𝑈 ) ) ∈ ∩ 𝑦 ∈ 𝑧 X 𝑥 ∈ 𝐼 if ( 𝑥 = 𝑦 , 𝐶 , ∪ 𝐽 ) ↔ ∀ 𝑦 ∈ 𝑧 ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝑧 , ( 𝑓 ‘ 𝑥 ) , 𝑈 ) ) ∈ X 𝑥 ∈ 𝐼 if ( 𝑥 = 𝑦 , 𝐶 , ∪ 𝐽 ) ) )
132 126 131 mpbird ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin ) ) ∧ ∀ 𝑥 ∈ 𝑧 ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) → ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝑧 , ( 𝑓 ‘ 𝑥 ) , 𝑈 ) ) ∈ ∩ 𝑦 ∈ 𝑧 X 𝑥 ∈ 𝐼 if ( 𝑥 = 𝑦 , 𝐶 , ∪ 𝐽 ) )
133 92 132 elind ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin ) ) ∧ ∀ 𝑥 ∈ 𝑧 ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) → ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝑧 , ( 𝑓 ‘ 𝑥 ) , 𝑈 ) ) ∈ ( X 𝑥 ∈ 𝐼 ∪ 𝐽 ∩ ∩ 𝑦 ∈ 𝑧 X 𝑥 ∈ 𝐼 if ( 𝑥 = 𝑦 , 𝐶 , ∪ 𝐽 ) ) )
134 133 ne0d ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin ) ) ∧ ∀ 𝑥 ∈ 𝑧 ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) → ( X 𝑥 ∈ 𝐼 ∪ 𝐽 ∩ ∩ 𝑦 ∈ 𝑧 X 𝑥 ∈ 𝐼 if ( 𝑥 = 𝑦 , 𝐶 , ∪ 𝐽 ) ) ≠ ∅ )
135 60 134 eqnetrd ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin ) ) ∧ ∀ 𝑥 ∈ 𝑧 ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) → ( ∪ ( ∏t ‘ ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) ) ∩ ∩ 𝑦 ∈ 𝑧 X 𝑥 ∈ 𝐼 if ( 𝑥 = 𝑦 , 𝐶 , ∪ 𝐽 ) ) ≠ ∅ )
136 135 adantrl ⊢ ( ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin ) ) ∧ ( 𝑓 : 𝑧 ⟶ V ∧ ∀ 𝑥 ∈ 𝑧 ( 𝑓 ‘ 𝑥 ) ∈ 𝐶 ) ) → ( ∪ ( ∏t ‘ ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) ) ∩ ∩ 𝑦 ∈ 𝑧 X 𝑥 ∈ 𝐼 if ( 𝑥 = 𝑦 , 𝐶 , ∪ 𝐽 ) ) ≠ ∅ )
137 57 136 exlimddv ⊢ ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin ) ) → ( ∪ ( ∏t ‘ ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) ) ∩ ∩ 𝑦 ∈ 𝑧 X 𝑥 ∈ 𝐼 if ( 𝑥 = 𝑦 , 𝐶 , ∪ 𝐽 ) ) ≠ ∅ )
138 28 6 33 137 cmpfiiin ⊢ ( 𝜑 → ( ∪ ( ∏t ‘ ( 𝑥 ∈ 𝐼 ↦ 𝐽 ) ) ∩ ∩ 𝑦 ∈ 𝐼 X 𝑥 ∈ 𝐼 if ( 𝑥 = 𝑦 , 𝐶 , ∪ 𝐽 ) ) ≠ ∅ )
139 27 138 eqnetrd ⊢ ( 𝜑 → ( X 𝑥 ∈ 𝐼 ∪ 𝐽 ∩ ∩ 𝑦 ∈ 𝐼 X 𝑥 ∈ 𝐼 if ( 𝑥 = 𝑦 , 𝐶 , ∪ 𝐽 ) ) ≠ ∅ )
140 12 139 eqnetrd ⊢ ( 𝜑 → X 𝑥 ∈ 𝐼 𝐶 ≠ ∅ )
141 n0 ⊢ ( X 𝑥 ∈ 𝐼 𝐶 ≠ ∅ ↔ ∃ 𝑦 𝑦 ∈ X 𝑥 ∈ 𝐼 𝐶 )
142 140 141 sylib ⊢ ( 𝜑 → ∃ 𝑦 𝑦 ∈ X 𝑥 ∈ 𝐼 𝐶 )
143 elixp2 ⊢ ( 𝑦 ∈ X 𝑥 ∈ 𝐼 𝐶 ↔ ( 𝑦 ∈ V ∧ 𝑦 Fn 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑦 ‘ 𝑥 ) ∈ 𝐶 ) )
144 143 simp3bi ⊢ ( 𝑦 ∈ X 𝑥 ∈ 𝐼 𝐶 → ∀ 𝑥 ∈ 𝐼 ( 𝑦 ‘ 𝑥 ) ∈ 𝐶 )
145 f1ocnv ⊢ ( 𝐵 : 𝑆 –1-1-onto→ 𝐶 → ◡ 𝐵 : 𝐶 –1-1-onto→ 𝑆 )
146 f1of ⊢ ( ◡ 𝐵 : 𝐶 –1-1-onto→ 𝑆 → ◡ 𝐵 : 𝐶 ⟶ 𝑆 )
147 ffvelcdm ⊢ ( ( ◡ 𝐵 : 𝐶 ⟶ 𝑆 ∧ ( 𝑦 ‘ 𝑥 ) ∈ 𝐶 ) → ( ◡ 𝐵 ‘ ( 𝑦 ‘ 𝑥 ) ) ∈ 𝑆 )
148 147 ex ⊢ ( ◡ 𝐵 : 𝐶 ⟶ 𝑆 → ( ( 𝑦 ‘ 𝑥 ) ∈ 𝐶 → ( ◡ 𝐵 ‘ ( 𝑦 ‘ 𝑥 ) ) ∈ 𝑆 ) )
149 4 145 146 148 4syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑦 ‘ 𝑥 ) ∈ 𝐶 → ( ◡ 𝐵 ‘ ( 𝑦 ‘ 𝑥 ) ) ∈ 𝑆 ) )
150 149 ralimdva ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐼 ( 𝑦 ‘ 𝑥 ) ∈ 𝐶 → ∀ 𝑥 ∈ 𝐼 ( ◡ 𝐵 ‘ ( 𝑦 ‘ 𝑥 ) ) ∈ 𝑆 ) )
151 150 imp ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑦 ‘ 𝑥 ) ∈ 𝐶 ) → ∀ 𝑥 ∈ 𝐼 ( ◡ 𝐵 ‘ ( 𝑦 ‘ 𝑥 ) ) ∈ 𝑆 )
152 144 151 sylan2 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ X 𝑥 ∈ 𝐼 𝐶 ) → ∀ 𝑥 ∈ 𝐼 ( ◡ 𝐵 ‘ ( 𝑦 ‘ 𝑥 ) ) ∈ 𝑆 )
153 mptelixpg ⊢ ( 𝐼 ∈ V → ( ( 𝑥 ∈ 𝐼 ↦ ( ◡ 𝐵 ‘ ( 𝑦 ‘ 𝑥 ) ) ) ∈ X 𝑥 ∈ 𝐼 𝑆 ↔ ∀ 𝑥 ∈ 𝐼 ( ◡ 𝐵 ‘ ( 𝑦 ‘ 𝑥 ) ) ∈ 𝑆 ) )
154 22 153 syl ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐼 ↦ ( ◡ 𝐵 ‘ ( 𝑦 ‘ 𝑥 ) ) ) ∈ X 𝑥 ∈ 𝐼 𝑆 ↔ ∀ 𝑥 ∈ 𝐼 ( ◡ 𝐵 ‘ ( 𝑦 ‘ 𝑥 ) ) ∈ 𝑆 ) )
155 154 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ X 𝑥 ∈ 𝐼 𝐶 ) → ( ( 𝑥 ∈ 𝐼 ↦ ( ◡ 𝐵 ‘ ( 𝑦 ‘ 𝑥 ) ) ) ∈ X 𝑥 ∈ 𝐼 𝑆 ↔ ∀ 𝑥 ∈ 𝐼 ( ◡ 𝐵 ‘ ( 𝑦 ‘ 𝑥 ) ) ∈ 𝑆 ) )
156 152 155 mpbird ⊢ ( ( 𝜑 ∧ 𝑦 ∈ X 𝑥 ∈ 𝐼 𝐶 ) → ( 𝑥 ∈ 𝐼 ↦ ( ◡ 𝐵 ‘ ( 𝑦 ‘ 𝑥 ) ) ) ∈ X 𝑥 ∈ 𝐼 𝑆 )
157 156 ne0d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ X 𝑥 ∈ 𝐼 𝐶 ) → X 𝑥 ∈ 𝐼 𝑆 ≠ ∅ )
158 142 157 exlimddv ⊢ ( 𝜑 → X 𝑥 ∈ 𝐼 𝑆 ≠ ∅ )