| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | kelac1.c | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐶 ∈ (Clsd‘𝐽)) | 
| 2 |  | eqid 2736 | . . . . . . . 8
⊢ ∪ 𝐽 =
∪ 𝐽 | 
| 3 | 2 | cldss 23038 | . . . . . . 7
⊢ (𝐶 ∈ (Clsd‘𝐽) → 𝐶 ⊆ ∪ 𝐽) | 
| 4 | 1, 3 | syl 17 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐶 ⊆ ∪ 𝐽) | 
| 5 | 4 | ralrimiva 3145 | . . . . 5
⊢ (𝜑 → ∀𝑥 ∈ 𝐼 𝐶 ⊆ ∪ 𝐽) | 
| 6 |  | boxriin 8981 | . . . . 5
⊢
(∀𝑥 ∈
𝐼 𝐶 ⊆ ∪ 𝐽 → X𝑥 ∈
𝐼 𝐶 = (X𝑥 ∈ 𝐼 ∪ 𝐽 ∩ ∩ 𝑦 ∈ 𝐼 X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽))) | 
| 7 | 5, 6 | syl 17 | . . . 4
⊢ (𝜑 → X𝑥 ∈
𝐼 𝐶 = (X𝑥 ∈ 𝐼 ∪ 𝐽 ∩ ∩ 𝑦 ∈ 𝐼 X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽))) | 
| 8 |  | kelac1.k | . . . . . . . . 9
⊢ (𝜑 →
(∏t‘(𝑥 ∈ 𝐼 ↦ 𝐽)) ∈ Comp) | 
| 9 |  | cmptop 23404 | . . . . . . . . 9
⊢
((∏t‘(𝑥 ∈ 𝐼 ↦ 𝐽)) ∈ Comp →
(∏t‘(𝑥 ∈ 𝐼 ↦ 𝐽)) ∈ Top) | 
| 10 |  | 0ntop 22912 | . . . . . . . . . . 11
⊢  ¬
∅ ∈ Top | 
| 11 |  | fvprc 6897 | . . . . . . . . . . . 12
⊢ (¬
(𝑥 ∈ 𝐼 ↦ 𝐽) ∈ V →
(∏t‘(𝑥 ∈ 𝐼 ↦ 𝐽)) = ∅) | 
| 12 | 11 | eleq1d 2825 | . . . . . . . . . . 11
⊢ (¬
(𝑥 ∈ 𝐼 ↦ 𝐽) ∈ V →
((∏t‘(𝑥 ∈ 𝐼 ↦ 𝐽)) ∈ Top ↔ ∅ ∈
Top)) | 
| 13 | 10, 12 | mtbiri 327 | . . . . . . . . . 10
⊢ (¬
(𝑥 ∈ 𝐼 ↦ 𝐽) ∈ V → ¬
(∏t‘(𝑥 ∈ 𝐼 ↦ 𝐽)) ∈ Top) | 
| 14 | 13 | con4i 114 | . . . . . . . . 9
⊢
((∏t‘(𝑥 ∈ 𝐼 ↦ 𝐽)) ∈ Top → (𝑥 ∈ 𝐼 ↦ 𝐽) ∈ V) | 
| 15 | 8, 9, 14 | 3syl 18 | . . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ 𝐽) ∈ V) | 
| 16 |  | kelac1.j | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐽 ∈ Top) | 
| 17 | 16 | fmpttd 7134 | . . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ 𝐽):𝐼⟶Top) | 
| 18 |  | dmfex 7928 | . . . . . . . 8
⊢ (((𝑥 ∈ 𝐼 ↦ 𝐽) ∈ V ∧ (𝑥 ∈ 𝐼 ↦ 𝐽):𝐼⟶Top) → 𝐼 ∈ V) | 
| 19 | 15, 17, 18 | syl2anc 584 | . . . . . . 7
⊢ (𝜑 → 𝐼 ∈ V) | 
| 20 | 16 | ralrimiva 3145 | . . . . . . 7
⊢ (𝜑 → ∀𝑥 ∈ 𝐼 𝐽 ∈ Top) | 
| 21 |  | eqid 2736 | . . . . . . . 8
⊢
(∏t‘(𝑥 ∈ 𝐼 ↦ 𝐽)) = (∏t‘(𝑥 ∈ 𝐼 ↦ 𝐽)) | 
| 22 | 21 | ptunimpt 23604 | . . . . . . 7
⊢ ((𝐼 ∈ V ∧ ∀𝑥 ∈ 𝐼 𝐽 ∈ Top) → X𝑥 ∈
𝐼 ∪ 𝐽 =
∪ (∏t‘(𝑥 ∈ 𝐼 ↦ 𝐽))) | 
| 23 | 19, 20, 22 | syl2anc 584 | . . . . . 6
⊢ (𝜑 → X𝑥 ∈
𝐼 ∪ 𝐽 =
∪ (∏t‘(𝑥 ∈ 𝐼 ↦ 𝐽))) | 
| 24 | 23 | ineq1d 4218 | . . . . 5
⊢ (𝜑 → (X𝑥 ∈
𝐼 ∪ 𝐽
∩ ∩ 𝑦 ∈ 𝐼 X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)) = (∪ (∏t‘(𝑥 ∈ 𝐼 ↦ 𝐽)) ∩ ∩
𝑦 ∈ 𝐼 X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽))) | 
| 25 |  | eqid 2736 | . . . . . 6
⊢ ∪ (∏t‘(𝑥 ∈ 𝐼 ↦ 𝐽)) = ∪
(∏t‘(𝑥 ∈ 𝐼 ↦ 𝐽)) | 
| 26 | 2 | topcld 23044 | . . . . . . . . . 10
⊢ (𝐽 ∈ Top → ∪ 𝐽
∈ (Clsd‘𝐽)) | 
| 27 | 16, 26 | syl 17 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ∪ 𝐽 ∈ (Clsd‘𝐽)) | 
| 28 | 1, 27 | ifcld 4571 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → if(𝑥 = 𝑦, 𝐶, ∪ 𝐽) ∈ (Clsd‘𝐽)) | 
| 29 | 19, 16, 28 | ptcldmpt 23623 | . . . . . . 7
⊢ (𝜑 → X𝑥 ∈
𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽) ∈
(Clsd‘(∏t‘(𝑥 ∈ 𝐼 ↦ 𝐽)))) | 
| 30 | 29 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽) ∈
(Clsd‘(∏t‘(𝑥 ∈ 𝐼 ↦ 𝐽)))) | 
| 31 |  | simprr 772 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) → 𝑧 ∈ Fin) | 
| 32 |  | kelac1.b | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐵:𝑆–1-1-onto→𝐶) | 
| 33 |  | f1ofo 6854 | . . . . . . . . . . . . . . 15
⊢ (𝐵:𝑆–1-1-onto→𝐶 → 𝐵:𝑆–onto→𝐶) | 
| 34 |  | foima 6824 | . . . . . . . . . . . . . . 15
⊢ (𝐵:𝑆–onto→𝐶 → (𝐵 “ 𝑆) = 𝐶) | 
| 35 | 32, 33, 34 | 3syl 18 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝐵 “ 𝑆) = 𝐶) | 
| 36 | 35 | eqcomd 2742 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐶 = (𝐵 “ 𝑆)) | 
| 37 |  | kelac1.z | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑆 ≠ ∅) | 
| 38 |  | f1ofn 6848 | . . . . . . . . . . . . . . . . 17
⊢ (𝐵:𝑆–1-1-onto→𝐶 → 𝐵 Fn 𝑆) | 
| 39 | 32, 38 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐵 Fn 𝑆) | 
| 40 |  | ssid 4005 | . . . . . . . . . . . . . . . 16
⊢ 𝑆 ⊆ 𝑆 | 
| 41 |  | fnimaeq0 6700 | . . . . . . . . . . . . . . . 16
⊢ ((𝐵 Fn 𝑆 ∧ 𝑆 ⊆ 𝑆) → ((𝐵 “ 𝑆) = ∅ ↔ 𝑆 = ∅)) | 
| 42 | 39, 40, 41 | sylancl 586 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝐵 “ 𝑆) = ∅ ↔ 𝑆 = ∅)) | 
| 43 | 42 | necon3bid 2984 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝐵 “ 𝑆) ≠ ∅ ↔ 𝑆 ≠ ∅)) | 
| 44 | 37, 43 | mpbird 257 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝐵 “ 𝑆) ≠ ∅) | 
| 45 | 36, 44 | eqnetrd 3007 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐶 ≠ ∅) | 
| 46 |  | n0 4352 | . . . . . . . . . . . 12
⊢ (𝐶 ≠ ∅ ↔
∃𝑤 𝑤 ∈ 𝐶) | 
| 47 | 45, 46 | sylib 218 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ∃𝑤 𝑤 ∈ 𝐶) | 
| 48 |  | rexv 3508 | . . . . . . . . . . 11
⊢
(∃𝑤 ∈ V
𝑤 ∈ 𝐶 ↔ ∃𝑤 𝑤 ∈ 𝐶) | 
| 49 | 47, 48 | sylibr 234 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ∃𝑤 ∈ V 𝑤 ∈ 𝐶) | 
| 50 | 49 | ralrimiva 3145 | . . . . . . . . 9
⊢ (𝜑 → ∀𝑥 ∈ 𝐼 ∃𝑤 ∈ V 𝑤 ∈ 𝐶) | 
| 51 |  | ssralv 4051 | . . . . . . . . . 10
⊢ (𝑧 ⊆ 𝐼 → (∀𝑥 ∈ 𝐼 ∃𝑤 ∈ V 𝑤 ∈ 𝐶 → ∀𝑥 ∈ 𝑧 ∃𝑤 ∈ V 𝑤 ∈ 𝐶)) | 
| 52 | 51 | adantr 480 | . . . . . . . . 9
⊢ ((𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin) → (∀𝑥 ∈ 𝐼 ∃𝑤 ∈ V 𝑤 ∈ 𝐶 → ∀𝑥 ∈ 𝑧 ∃𝑤 ∈ V 𝑤 ∈ 𝐶)) | 
| 53 | 50, 52 | mpan9 506 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) → ∀𝑥 ∈ 𝑧 ∃𝑤 ∈ V 𝑤 ∈ 𝐶) | 
| 54 |  | eleq1 2828 | . . . . . . . . 9
⊢ (𝑤 = (𝑓‘𝑥) → (𝑤 ∈ 𝐶 ↔ (𝑓‘𝑥) ∈ 𝐶)) | 
| 55 | 54 | ac6sfi 9321 | . . . . . . . 8
⊢ ((𝑧 ∈ Fin ∧ ∀𝑥 ∈ 𝑧 ∃𝑤 ∈ V 𝑤 ∈ 𝐶) → ∃𝑓(𝑓:𝑧⟶V ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶)) | 
| 56 | 31, 53, 55 | syl2anc 584 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) → ∃𝑓(𝑓:𝑧⟶V ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶)) | 
| 57 | 23 | eqcomd 2742 | . . . . . . . . . . 11
⊢ (𝜑 → ∪ (∏t‘(𝑥 ∈ 𝐼 ↦ 𝐽)) = X𝑥 ∈ 𝐼 ∪ 𝐽) | 
| 58 | 57 | ineq1d 4218 | . . . . . . . . . 10
⊢ (𝜑 → (∪ (∏t‘(𝑥 ∈ 𝐼 ↦ 𝐽)) ∩ ∩
𝑦 ∈ 𝑧 X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)) = (X𝑥 ∈
𝐼 ∪ 𝐽
∩ ∩ 𝑦 ∈ 𝑧 X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽))) | 
| 59 | 58 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) → (∪
(∏t‘(𝑥 ∈ 𝐼 ↦ 𝐽)) ∩ ∩
𝑦 ∈ 𝑧 X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)) = (X𝑥 ∈
𝐼 ∪ 𝐽
∩ ∩ 𝑦 ∈ 𝑧 X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽))) | 
| 60 |  | iftrue 4530 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ 𝑧 → if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) = (𝑓‘𝑥)) | 
| 61 | 60 | ad2antrl 728 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ (𝑥 ∈ 𝑧 ∧ (𝑓‘𝑥) ∈ 𝐶)) → if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) = (𝑓‘𝑥)) | 
| 62 |  | simpll 766 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ 𝑥 ∈ 𝑧) → 𝜑) | 
| 63 |  | simprl 770 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) → 𝑧 ⊆ 𝐼) | 
| 64 | 63 | sselda 3982 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ 𝑥 ∈ 𝑧) → 𝑥 ∈ 𝐼) | 
| 65 | 62, 64, 4 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ 𝑥 ∈ 𝑧) → 𝐶 ⊆ ∪ 𝐽) | 
| 66 | 65 | sseld 3981 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ 𝑥 ∈ 𝑧) → ((𝑓‘𝑥) ∈ 𝐶 → (𝑓‘𝑥) ∈ ∪ 𝐽)) | 
| 67 | 66 | impr 454 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ (𝑥 ∈ 𝑧 ∧ (𝑓‘𝑥) ∈ 𝐶)) → (𝑓‘𝑥) ∈ ∪ 𝐽) | 
| 68 | 61, 67 | eqeltrd 2840 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ (𝑥 ∈ 𝑧 ∧ (𝑓‘𝑥) ∈ 𝐶)) → if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ ∪ 𝐽) | 
| 69 | 68 | expr 456 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ 𝑥 ∈ 𝑧) → ((𝑓‘𝑥) ∈ 𝐶 → if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ ∪ 𝐽)) | 
| 70 | 69 | ralimdva 3166 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) → (∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶 → ∀𝑥 ∈ 𝑧 if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ ∪ 𝐽)) | 
| 71 | 70 | imp 406 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) → ∀𝑥 ∈ 𝑧 if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ ∪ 𝐽) | 
| 72 |  | eldifn 4131 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ (𝐼 ∖ 𝑧) → ¬ 𝑥 ∈ 𝑧) | 
| 73 | 72 | iffalsed 4535 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ (𝐼 ∖ 𝑧) → if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) = 𝑈) | 
| 74 | 73 | adantl 481 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∖ 𝑧)) → if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) = 𝑈) | 
| 75 |  | eldifi 4130 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ (𝐼 ∖ 𝑧) → 𝑥 ∈ 𝐼) | 
| 76 |  | kelac1.u | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑈 ∈ ∪ 𝐽) | 
| 77 | 75, 76 | sylan2 593 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∖ 𝑧)) → 𝑈 ∈ ∪ 𝐽) | 
| 78 | 74, 77 | eqeltrd 2840 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∖ 𝑧)) → if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ ∪ 𝐽) | 
| 79 | 78 | ralrimiva 3145 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ∀𝑥 ∈ (𝐼 ∖ 𝑧)if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ ∪ 𝐽) | 
| 80 | 79 | ad2antrr 726 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) → ∀𝑥 ∈ (𝐼 ∖ 𝑧)if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ ∪ 𝐽) | 
| 81 |  | ralun 4197 | . . . . . . . . . . . . . 14
⊢
((∀𝑥 ∈
𝑧 if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ ∪ 𝐽 ∧ ∀𝑥 ∈ (𝐼 ∖ 𝑧)if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ ∪ 𝐽) → ∀𝑥 ∈ (𝑧 ∪ (𝐼 ∖ 𝑧))if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ ∪ 𝐽) | 
| 82 | 71, 80, 81 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) → ∀𝑥 ∈ (𝑧 ∪ (𝐼 ∖ 𝑧))if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ ∪ 𝐽) | 
| 83 |  | undif 4481 | . . . . . . . . . . . . . . . . 17
⊢ (𝑧 ⊆ 𝐼 ↔ (𝑧 ∪ (𝐼 ∖ 𝑧)) = 𝐼) | 
| 84 | 83 | biimpi 216 | . . . . . . . . . . . . . . . 16
⊢ (𝑧 ⊆ 𝐼 → (𝑧 ∪ (𝐼 ∖ 𝑧)) = 𝐼) | 
| 85 | 84 | ad2antrl 728 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) → (𝑧 ∪ (𝐼 ∖ 𝑧)) = 𝐼) | 
| 86 | 85 | raleqdv 3325 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) → (∀𝑥 ∈ (𝑧 ∪ (𝐼 ∖ 𝑧))if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ ∪ 𝐽 ↔ ∀𝑥 ∈ 𝐼 if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ ∪ 𝐽)) | 
| 87 | 86 | adantr 480 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) → (∀𝑥 ∈ (𝑧 ∪ (𝐼 ∖ 𝑧))if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ ∪ 𝐽 ↔ ∀𝑥 ∈ 𝐼 if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ ∪ 𝐽)) | 
| 88 | 82, 87 | mpbid 232 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) → ∀𝑥 ∈ 𝐼 if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ ∪ 𝐽) | 
| 89 | 19 | ad2antrr 726 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) → 𝐼 ∈ V) | 
| 90 |  | mptelixpg 8976 | . . . . . . . . . . . . 13
⊢ (𝐼 ∈ V → ((𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈)) ∈ X𝑥 ∈ 𝐼 ∪ 𝐽 ↔ ∀𝑥 ∈ 𝐼 if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ ∪ 𝐽)) | 
| 91 | 89, 90 | syl 17 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) → ((𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈)) ∈ X𝑥 ∈ 𝐼 ∪ 𝐽 ↔ ∀𝑥 ∈ 𝐼 if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ ∪ 𝐽)) | 
| 92 | 88, 91 | mpbird 257 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) → (𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈)) ∈ X𝑥 ∈ 𝐼 ∪ 𝐽) | 
| 93 |  | eleq2 2829 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐶 = if(𝑥 = 𝑦, 𝐶, ∪ 𝐽) → ((𝑓‘𝑥) ∈ 𝐶 ↔ (𝑓‘𝑥) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽))) | 
| 94 |  | eleq2 2829 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (∪ 𝐽 =
if(𝑥 = 𝑦, 𝐶, ∪ 𝐽) → ((𝑓‘𝑥) ∈ ∪ 𝐽 ↔ (𝑓‘𝑥) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽))) | 
| 95 |  | simplrr 777 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ (𝑥 ∈ 𝑧 ∧ (𝑓‘𝑥) ∈ 𝐶)) ∧ 𝑥 = 𝑦) → (𝑓‘𝑥) ∈ 𝐶) | 
| 96 | 67 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ (𝑥 ∈ 𝑧 ∧ (𝑓‘𝑥) ∈ 𝐶)) ∧ ¬ 𝑥 = 𝑦) → (𝑓‘𝑥) ∈ ∪ 𝐽) | 
| 97 | 93, 94, 95, 96 | ifbothda 4563 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ (𝑥 ∈ 𝑧 ∧ (𝑓‘𝑥) ∈ 𝐶)) → (𝑓‘𝑥) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)) | 
| 98 | 61, 97 | eqeltrd 2840 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ (𝑥 ∈ 𝑧 ∧ (𝑓‘𝑥) ∈ 𝐶)) → if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)) | 
| 99 | 98 | expr 456 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ 𝑥 ∈ 𝑧) → ((𝑓‘𝑥) ∈ 𝐶 → if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽))) | 
| 100 | 99 | ralimdva 3166 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) → (∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶 → ∀𝑥 ∈ 𝑧 if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽))) | 
| 101 | 100 | imp 406 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) → ∀𝑥 ∈ 𝑧 if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)) | 
| 102 | 101 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) ∧ 𝑦 ∈ 𝑧) → ∀𝑥 ∈ 𝑧 if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)) | 
| 103 | 77 | adantlr 715 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑧) ∧ 𝑥 ∈ (𝐼 ∖ 𝑧)) → 𝑈 ∈ ∪ 𝐽) | 
| 104 | 73 | adantl 481 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑧) ∧ 𝑥 ∈ (𝐼 ∖ 𝑧)) → if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) = 𝑈) | 
| 105 |  | disjdifr 4472 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐼 ∖ 𝑧) ∩ 𝑧) = ∅ | 
| 106 | 105 | a1i 11 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑧) ∧ 𝑥 ∈ (𝐼 ∖ 𝑧)) → ((𝐼 ∖ 𝑧) ∩ 𝑧) = ∅) | 
| 107 |  | simpr 484 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑧) ∧ 𝑥 ∈ (𝐼 ∖ 𝑧)) → 𝑥 ∈ (𝐼 ∖ 𝑧)) | 
| 108 |  | simplr 768 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑧) ∧ 𝑥 ∈ (𝐼 ∖ 𝑧)) → 𝑦 ∈ 𝑧) | 
| 109 |  | disjne 4454 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐼 ∖ 𝑧) ∩ 𝑧) = ∅ ∧ 𝑥 ∈ (𝐼 ∖ 𝑧) ∧ 𝑦 ∈ 𝑧) → 𝑥 ≠ 𝑦) | 
| 110 | 106, 107,
108, 109 | syl3anc 1372 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑧) ∧ 𝑥 ∈ (𝐼 ∖ 𝑧)) → 𝑥 ≠ 𝑦) | 
| 111 | 110 | neneqd 2944 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑧) ∧ 𝑥 ∈ (𝐼 ∖ 𝑧)) → ¬ 𝑥 = 𝑦) | 
| 112 | 111 | iffalsed 4535 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑧) ∧ 𝑥 ∈ (𝐼 ∖ 𝑧)) → if(𝑥 = 𝑦, 𝐶, ∪ 𝐽) = ∪
𝐽) | 
| 113 | 103, 104,
112 | 3eltr4d 2855 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑧) ∧ 𝑥 ∈ (𝐼 ∖ 𝑧)) → if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)) | 
| 114 | 113 | ralrimiva 3145 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑧) → ∀𝑥 ∈ (𝐼 ∖ 𝑧)if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)) | 
| 115 | 114 | adantlr 715 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ 𝑦 ∈ 𝑧) → ∀𝑥 ∈ (𝐼 ∖ 𝑧)if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)) | 
| 116 | 115 | adantlr 715 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) ∧ 𝑦 ∈ 𝑧) → ∀𝑥 ∈ (𝐼 ∖ 𝑧)if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)) | 
| 117 |  | ralun 4197 | . . . . . . . . . . . . . . . 16
⊢
((∀𝑥 ∈
𝑧 if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽) ∧ ∀𝑥 ∈ (𝐼 ∖ 𝑧)if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)) → ∀𝑥 ∈ (𝑧 ∪ (𝐼 ∖ 𝑧))if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)) | 
| 118 | 102, 116,
117 | syl2anc 584 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) ∧ 𝑦 ∈ 𝑧) → ∀𝑥 ∈ (𝑧 ∪ (𝐼 ∖ 𝑧))if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)) | 
| 119 | 85 | raleqdv 3325 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) → (∀𝑥 ∈ (𝑧 ∪ (𝐼 ∖ 𝑧))if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽) ↔ ∀𝑥 ∈ 𝐼 if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽))) | 
| 120 | 119 | ad2antrr 726 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) ∧ 𝑦 ∈ 𝑧) → (∀𝑥 ∈ (𝑧 ∪ (𝐼 ∖ 𝑧))if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽) ↔ ∀𝑥 ∈ 𝐼 if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽))) | 
| 121 | 118, 120 | mpbid 232 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) ∧ 𝑦 ∈ 𝑧) → ∀𝑥 ∈ 𝐼 if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)) | 
| 122 | 19 | ad3antrrr 730 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) ∧ 𝑦 ∈ 𝑧) → 𝐼 ∈ V) | 
| 123 |  | mptelixpg 8976 | . . . . . . . . . . . . . . 15
⊢ (𝐼 ∈ V → ((𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈)) ∈ X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽) ↔ ∀𝑥 ∈ 𝐼 if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽))) | 
| 124 | 122, 123 | syl 17 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) ∧ 𝑦 ∈ 𝑧) → ((𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈)) ∈ X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽) ↔ ∀𝑥 ∈ 𝐼 if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽))) | 
| 125 | 121, 124 | mpbird 257 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) ∧ 𝑦 ∈ 𝑧) → (𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈)) ∈ X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)) | 
| 126 | 125 | ralrimiva 3145 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) → ∀𝑦 ∈ 𝑧 (𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈)) ∈ X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)) | 
| 127 |  | mptexg 7242 | . . . . . . . . . . . . . . 15
⊢ (𝐼 ∈ V → (𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈)) ∈ V) | 
| 128 | 19, 127 | syl 17 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈)) ∈ V) | 
| 129 | 128 | ad2antrr 726 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) → (𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈)) ∈ V) | 
| 130 |  | eliin 4995 | . . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈)) ∈ V → ((𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈)) ∈ ∩ 𝑦 ∈ 𝑧 X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽) ↔ ∀𝑦 ∈ 𝑧 (𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈)) ∈ X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽))) | 
| 131 | 129, 130 | syl 17 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) → ((𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈)) ∈ ∩ 𝑦 ∈ 𝑧 X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽) ↔ ∀𝑦 ∈ 𝑧 (𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈)) ∈ X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽))) | 
| 132 | 126, 131 | mpbird 257 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) → (𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈)) ∈ ∩ 𝑦 ∈ 𝑧 X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)) | 
| 133 | 92, 132 | elind 4199 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) → (𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈)) ∈ (X𝑥 ∈ 𝐼 ∪ 𝐽 ∩ ∩ 𝑦 ∈ 𝑧 X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽))) | 
| 134 | 133 | ne0d 4341 | . . . . . . . . 9
⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) → (X𝑥 ∈ 𝐼 ∪ 𝐽 ∩ ∩ 𝑦 ∈ 𝑧 X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)) ≠
∅) | 
| 135 | 59, 134 | eqnetrd 3007 | . . . . . . . 8
⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) → (∪
(∏t‘(𝑥 ∈ 𝐼 ↦ 𝐽)) ∩ ∩
𝑦 ∈ 𝑧 X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)) ≠
∅) | 
| 136 | 135 | adantrl 716 | . . . . . . 7
⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ (𝑓:𝑧⟶V ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶)) → (∪
(∏t‘(𝑥 ∈ 𝐼 ↦ 𝐽)) ∩ ∩
𝑦 ∈ 𝑧 X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)) ≠
∅) | 
| 137 | 56, 136 | exlimddv 1934 | . . . . . 6
⊢ ((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) → (∪ (∏t‘(𝑥 ∈ 𝐼 ↦ 𝐽)) ∩ ∩
𝑦 ∈ 𝑧 X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)) ≠
∅) | 
| 138 | 25, 8, 30, 137 | cmpfiiin 42713 | . . . . 5
⊢ (𝜑 → (∪ (∏t‘(𝑥 ∈ 𝐼 ↦ 𝐽)) ∩ ∩
𝑦 ∈ 𝐼 X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)) ≠
∅) | 
| 139 | 24, 138 | eqnetrd 3007 | . . . 4
⊢ (𝜑 → (X𝑥 ∈
𝐼 ∪ 𝐽
∩ ∩ 𝑦 ∈ 𝐼 X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)) ≠
∅) | 
| 140 | 7, 139 | eqnetrd 3007 | . . 3
⊢ (𝜑 → X𝑥 ∈
𝐼 𝐶 ≠ ∅) | 
| 141 |  | n0 4352 | . . 3
⊢ (X𝑥 ∈
𝐼 𝐶 ≠ ∅ ↔ ∃𝑦 𝑦 ∈ X𝑥 ∈ 𝐼 𝐶) | 
| 142 | 140, 141 | sylib 218 | . 2
⊢ (𝜑 → ∃𝑦 𝑦 ∈ X𝑥 ∈ 𝐼 𝐶) | 
| 143 |  | elixp2 8942 | . . . . . 6
⊢ (𝑦 ∈ X𝑥 ∈
𝐼 𝐶 ↔ (𝑦 ∈ V ∧ 𝑦 Fn 𝐼 ∧ ∀𝑥 ∈ 𝐼 (𝑦‘𝑥) ∈ 𝐶)) | 
| 144 | 143 | simp3bi 1147 | . . . . 5
⊢ (𝑦 ∈ X𝑥 ∈
𝐼 𝐶 → ∀𝑥 ∈ 𝐼 (𝑦‘𝑥) ∈ 𝐶) | 
| 145 |  | f1ocnv 6859 | . . . . . . . 8
⊢ (𝐵:𝑆–1-1-onto→𝐶 → ◡𝐵:𝐶–1-1-onto→𝑆) | 
| 146 |  | f1of 6847 | . . . . . . . 8
⊢ (◡𝐵:𝐶–1-1-onto→𝑆 → ◡𝐵:𝐶⟶𝑆) | 
| 147 |  | ffvelcdm 7100 | . . . . . . . . 9
⊢ ((◡𝐵:𝐶⟶𝑆 ∧ (𝑦‘𝑥) ∈ 𝐶) → (◡𝐵‘(𝑦‘𝑥)) ∈ 𝑆) | 
| 148 | 147 | ex 412 | . . . . . . . 8
⊢ (◡𝐵:𝐶⟶𝑆 → ((𝑦‘𝑥) ∈ 𝐶 → (◡𝐵‘(𝑦‘𝑥)) ∈ 𝑆)) | 
| 149 | 32, 145, 146, 148 | 4syl 19 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝑦‘𝑥) ∈ 𝐶 → (◡𝐵‘(𝑦‘𝑥)) ∈ 𝑆)) | 
| 150 | 149 | ralimdva 3166 | . . . . . 6
⊢ (𝜑 → (∀𝑥 ∈ 𝐼 (𝑦‘𝑥) ∈ 𝐶 → ∀𝑥 ∈ 𝐼 (◡𝐵‘(𝑦‘𝑥)) ∈ 𝑆)) | 
| 151 | 150 | imp 406 | . . . . 5
⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐼 (𝑦‘𝑥) ∈ 𝐶) → ∀𝑥 ∈ 𝐼 (◡𝐵‘(𝑦‘𝑥)) ∈ 𝑆) | 
| 152 | 144, 151 | sylan2 593 | . . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ X𝑥 ∈ 𝐼 𝐶) → ∀𝑥 ∈ 𝐼 (◡𝐵‘(𝑦‘𝑥)) ∈ 𝑆) | 
| 153 |  | mptelixpg 8976 | . . . . . 6
⊢ (𝐼 ∈ V → ((𝑥 ∈ 𝐼 ↦ (◡𝐵‘(𝑦‘𝑥))) ∈ X𝑥 ∈ 𝐼 𝑆 ↔ ∀𝑥 ∈ 𝐼 (◡𝐵‘(𝑦‘𝑥)) ∈ 𝑆)) | 
| 154 | 19, 153 | syl 17 | . . . . 5
⊢ (𝜑 → ((𝑥 ∈ 𝐼 ↦ (◡𝐵‘(𝑦‘𝑥))) ∈ X𝑥 ∈ 𝐼 𝑆 ↔ ∀𝑥 ∈ 𝐼 (◡𝐵‘(𝑦‘𝑥)) ∈ 𝑆)) | 
| 155 | 154 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ X𝑥 ∈ 𝐼 𝐶) → ((𝑥 ∈ 𝐼 ↦ (◡𝐵‘(𝑦‘𝑥))) ∈ X𝑥 ∈ 𝐼 𝑆 ↔ ∀𝑥 ∈ 𝐼 (◡𝐵‘(𝑦‘𝑥)) ∈ 𝑆)) | 
| 156 | 152, 155 | mpbird 257 | . . 3
⊢ ((𝜑 ∧ 𝑦 ∈ X𝑥 ∈ 𝐼 𝐶) → (𝑥 ∈ 𝐼 ↦ (◡𝐵‘(𝑦‘𝑥))) ∈ X𝑥 ∈ 𝐼 𝑆) | 
| 157 | 156 | ne0d 4341 | . 2
⊢ ((𝜑 ∧ 𝑦 ∈ X𝑥 ∈ 𝐼 𝐶) → X𝑥 ∈ 𝐼 𝑆 ≠ ∅) | 
| 158 | 142, 157 | exlimddv 1934 | 1
⊢ (𝜑 → X𝑥 ∈
𝐼 𝑆 ≠ ∅) |