| Step | Hyp | Ref
| Expression |
| 1 | | elex 3501 |
. 2
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V) |
| 2 | | vex 3484 |
. . . . . . . . . 10
⊢ 𝑡 ∈ V |
| 3 | | elfi 9453 |
. . . . . . . . . 10
⊢ ((𝑡 ∈ V ∧ 𝐴 ∈ V) → (𝑡 ∈ (fi‘𝐴) ↔ ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)𝑡 = ∩ 𝑥)) |
| 4 | 2, 3 | mpan 690 |
. . . . . . . . 9
⊢ (𝐴 ∈ V → (𝑡 ∈ (fi‘𝐴) ↔ ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)𝑡 = ∩ 𝑥)) |
| 5 | 4 | biimpd 229 |
. . . . . . . 8
⊢ (𝐴 ∈ V → (𝑡 ∈ (fi‘𝐴) → ∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)𝑡 = ∩ 𝑥)) |
| 6 | | df-rex 3071 |
. . . . . . . . 9
⊢
(∃𝑥 ∈
(𝒫 𝐴 ∩
Fin)𝑡 = ∩ 𝑥
↔ ∃𝑥(𝑥 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑡 = ∩
𝑥)) |
| 7 | | fiint 9366 |
. . . . . . . . . . . 12
⊢
(∀𝑥 ∈
𝑧 ∀𝑦 ∈ 𝑧 (𝑥 ∩ 𝑦) ∈ 𝑧 ↔ ∀𝑥((𝑥 ⊆ 𝑧 ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin) → ∩ 𝑥
∈ 𝑧)) |
| 8 | | elinel1 4201 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ (𝒫 𝐴 ∩ Fin) → 𝑥 ∈ 𝒫 𝐴) |
| 9 | 8 | elpwid 4609 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ (𝒫 𝐴 ∩ Fin) → 𝑥 ⊆ 𝐴) |
| 10 | 9 | 3ad2ant2 1135 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ⊆ 𝑧 ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑡 = ∩ 𝑥) → 𝑥 ⊆ 𝐴) |
| 11 | | simp1 1137 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ⊆ 𝑧 ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑡 = ∩ 𝑥) → 𝐴 ⊆ 𝑧) |
| 12 | 10, 11 | sstrd 3994 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ⊆ 𝑧 ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑡 = ∩ 𝑥) → 𝑥 ⊆ 𝑧) |
| 13 | | eqvisset 3500 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑡 = ∩
𝑥 → ∩ 𝑥
∈ V) |
| 14 | | intex 5344 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ≠ ∅ ↔ ∩ 𝑥
∈ V) |
| 15 | 13, 14 | sylibr 234 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑡 = ∩
𝑥 → 𝑥 ≠ ∅) |
| 16 | 15 | 3ad2ant3 1136 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ⊆ 𝑧 ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑡 = ∩ 𝑥) → 𝑥 ≠ ∅) |
| 17 | | elinel2 4202 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ (𝒫 𝐴 ∩ Fin) → 𝑥 ∈ Fin) |
| 18 | 17 | 3ad2ant2 1135 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ⊆ 𝑧 ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑡 = ∩ 𝑥) → 𝑥 ∈ Fin) |
| 19 | 12, 16, 18 | 3jca 1129 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ⊆ 𝑧 ∧ 𝑥 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑡 = ∩ 𝑥) → (𝑥 ⊆ 𝑧 ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin)) |
| 20 | 19 | 3expib 1123 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ⊆ 𝑧 → ((𝑥 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑡 = ∩ 𝑥) → (𝑥 ⊆ 𝑧 ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin))) |
| 21 | | pm2.27 42 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ⊆ 𝑧 ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin) → (((𝑥 ⊆ 𝑧 ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin) → ∩ 𝑥
∈ 𝑧) → ∩ 𝑥
∈ 𝑧)) |
| 22 | 20, 21 | syl6 35 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ⊆ 𝑧 → ((𝑥 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑡 = ∩ 𝑥) → (((𝑥 ⊆ 𝑧 ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin) → ∩ 𝑥
∈ 𝑧) → ∩ 𝑥
∈ 𝑧))) |
| 23 | | eleq1 2829 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑡 = ∩
𝑥 → (𝑡 ∈ 𝑧 ↔ ∩ 𝑥 ∈ 𝑧)) |
| 24 | 23 | biimprd 248 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑡 = ∩
𝑥 → (∩ 𝑥
∈ 𝑧 → 𝑡 ∈ 𝑧)) |
| 25 | 24 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑡 = ∩
𝑥) → (∩ 𝑥
∈ 𝑧 → 𝑡 ∈ 𝑧)) |
| 26 | 25 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ⊆ 𝑧 → ((𝑥 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑡 = ∩ 𝑥) → (∩ 𝑥
∈ 𝑧 → 𝑡 ∈ 𝑧))) |
| 27 | 22, 26 | syldd 72 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ⊆ 𝑧 → ((𝑥 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑡 = ∩ 𝑥) → (((𝑥 ⊆ 𝑧 ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin) → ∩ 𝑥
∈ 𝑧) → 𝑡 ∈ 𝑧))) |
| 28 | 27 | com23 86 |
. . . . . . . . . . . . 13
⊢ (𝐴 ⊆ 𝑧 → (((𝑥 ⊆ 𝑧 ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin) → ∩ 𝑥
∈ 𝑧) → ((𝑥 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑡 = ∩
𝑥) → 𝑡 ∈ 𝑧))) |
| 29 | 28 | alimdv 1916 |
. . . . . . . . . . . 12
⊢ (𝐴 ⊆ 𝑧 → (∀𝑥((𝑥 ⊆ 𝑧 ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin) → ∩ 𝑥
∈ 𝑧) →
∀𝑥((𝑥 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑡 = ∩
𝑥) → 𝑡 ∈ 𝑧))) |
| 30 | 7, 29 | biimtrid 242 |
. . . . . . . . . . 11
⊢ (𝐴 ⊆ 𝑧 → (∀𝑥 ∈ 𝑧 ∀𝑦 ∈ 𝑧 (𝑥 ∩ 𝑦) ∈ 𝑧 → ∀𝑥((𝑥 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑡 = ∩ 𝑥) → 𝑡 ∈ 𝑧))) |
| 31 | 30 | imp 406 |
. . . . . . . . . 10
⊢ ((𝐴 ⊆ 𝑧 ∧ ∀𝑥 ∈ 𝑧 ∀𝑦 ∈ 𝑧 (𝑥 ∩ 𝑦) ∈ 𝑧) → ∀𝑥((𝑥 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑡 = ∩ 𝑥) → 𝑡 ∈ 𝑧)) |
| 32 | | 19.23v 1942 |
. . . . . . . . . 10
⊢
(∀𝑥((𝑥 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑡 = ∩
𝑥) → 𝑡 ∈ 𝑧) ↔ (∃𝑥(𝑥 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑡 = ∩ 𝑥) → 𝑡 ∈ 𝑧)) |
| 33 | 31, 32 | sylib 218 |
. . . . . . . . 9
⊢ ((𝐴 ⊆ 𝑧 ∧ ∀𝑥 ∈ 𝑧 ∀𝑦 ∈ 𝑧 (𝑥 ∩ 𝑦) ∈ 𝑧) → (∃𝑥(𝑥 ∈ (𝒫 𝐴 ∩ Fin) ∧ 𝑡 = ∩ 𝑥) → 𝑡 ∈ 𝑧)) |
| 34 | 6, 33 | biimtrid 242 |
. . . . . . . 8
⊢ ((𝐴 ⊆ 𝑧 ∧ ∀𝑥 ∈ 𝑧 ∀𝑦 ∈ 𝑧 (𝑥 ∩ 𝑦) ∈ 𝑧) → (∃𝑥 ∈ (𝒫 𝐴 ∩ Fin)𝑡 = ∩ 𝑥 → 𝑡 ∈ 𝑧)) |
| 35 | 5, 34 | sylan9 507 |
. . . . . . 7
⊢ ((𝐴 ∈ V ∧ (𝐴 ⊆ 𝑧 ∧ ∀𝑥 ∈ 𝑧 ∀𝑦 ∈ 𝑧 (𝑥 ∩ 𝑦) ∈ 𝑧)) → (𝑡 ∈ (fi‘𝐴) → 𝑡 ∈ 𝑧)) |
| 36 | 35 | ssrdv 3989 |
. . . . . 6
⊢ ((𝐴 ∈ V ∧ (𝐴 ⊆ 𝑧 ∧ ∀𝑥 ∈ 𝑧 ∀𝑦 ∈ 𝑧 (𝑥 ∩ 𝑦) ∈ 𝑧)) → (fi‘𝐴) ⊆ 𝑧) |
| 37 | 36 | ex 412 |
. . . . 5
⊢ (𝐴 ∈ V → ((𝐴 ⊆ 𝑧 ∧ ∀𝑥 ∈ 𝑧 ∀𝑦 ∈ 𝑧 (𝑥 ∩ 𝑦) ∈ 𝑧) → (fi‘𝐴) ⊆ 𝑧)) |
| 38 | 37 | alrimiv 1927 |
. . . 4
⊢ (𝐴 ∈ V → ∀𝑧((𝐴 ⊆ 𝑧 ∧ ∀𝑥 ∈ 𝑧 ∀𝑦 ∈ 𝑧 (𝑥 ∩ 𝑦) ∈ 𝑧) → (fi‘𝐴) ⊆ 𝑧)) |
| 39 | | ssintab 4965 |
. . . 4
⊢
((fi‘𝐴)
⊆ ∩ {𝑧 ∣ (𝐴 ⊆ 𝑧 ∧ ∀𝑥 ∈ 𝑧 ∀𝑦 ∈ 𝑧 (𝑥 ∩ 𝑦) ∈ 𝑧)} ↔ ∀𝑧((𝐴 ⊆ 𝑧 ∧ ∀𝑥 ∈ 𝑧 ∀𝑦 ∈ 𝑧 (𝑥 ∩ 𝑦) ∈ 𝑧) → (fi‘𝐴) ⊆ 𝑧)) |
| 40 | 38, 39 | sylibr 234 |
. . 3
⊢ (𝐴 ∈ V → (fi‘𝐴) ⊆ ∩ {𝑧
∣ (𝐴 ⊆ 𝑧 ∧ ∀𝑥 ∈ 𝑧 ∀𝑦 ∈ 𝑧 (𝑥 ∩ 𝑦) ∈ 𝑧)}) |
| 41 | | ssfii 9459 |
. . . . 5
⊢ (𝐴 ∈ V → 𝐴 ⊆ (fi‘𝐴)) |
| 42 | | fiin 9462 |
. . . . . 6
⊢ ((𝑥 ∈ (fi‘𝐴) ∧ 𝑦 ∈ (fi‘𝐴)) → (𝑥 ∩ 𝑦) ∈ (fi‘𝐴)) |
| 43 | 42 | rgen2 3199 |
. . . . 5
⊢
∀𝑥 ∈
(fi‘𝐴)∀𝑦 ∈ (fi‘𝐴)(𝑥 ∩ 𝑦) ∈ (fi‘𝐴) |
| 44 | | fvex 6919 |
. . . . . 6
⊢
(fi‘𝐴) ∈
V |
| 45 | | sseq2 4010 |
. . . . . . 7
⊢ (𝑧 = (fi‘𝐴) → (𝐴 ⊆ 𝑧 ↔ 𝐴 ⊆ (fi‘𝐴))) |
| 46 | | eleq2 2830 |
. . . . . . . . 9
⊢ (𝑧 = (fi‘𝐴) → ((𝑥 ∩ 𝑦) ∈ 𝑧 ↔ (𝑥 ∩ 𝑦) ∈ (fi‘𝐴))) |
| 47 | 46 | raleqbi1dv 3338 |
. . . . . . . 8
⊢ (𝑧 = (fi‘𝐴) → (∀𝑦 ∈ 𝑧 (𝑥 ∩ 𝑦) ∈ 𝑧 ↔ ∀𝑦 ∈ (fi‘𝐴)(𝑥 ∩ 𝑦) ∈ (fi‘𝐴))) |
| 48 | 47 | raleqbi1dv 3338 |
. . . . . . 7
⊢ (𝑧 = (fi‘𝐴) → (∀𝑥 ∈ 𝑧 ∀𝑦 ∈ 𝑧 (𝑥 ∩ 𝑦) ∈ 𝑧 ↔ ∀𝑥 ∈ (fi‘𝐴)∀𝑦 ∈ (fi‘𝐴)(𝑥 ∩ 𝑦) ∈ (fi‘𝐴))) |
| 49 | 45, 48 | anbi12d 632 |
. . . . . 6
⊢ (𝑧 = (fi‘𝐴) → ((𝐴 ⊆ 𝑧 ∧ ∀𝑥 ∈ 𝑧 ∀𝑦 ∈ 𝑧 (𝑥 ∩ 𝑦) ∈ 𝑧) ↔ (𝐴 ⊆ (fi‘𝐴) ∧ ∀𝑥 ∈ (fi‘𝐴)∀𝑦 ∈ (fi‘𝐴)(𝑥 ∩ 𝑦) ∈ (fi‘𝐴)))) |
| 50 | 44, 49 | elab 3679 |
. . . . 5
⊢
((fi‘𝐴) ∈
{𝑧 ∣ (𝐴 ⊆ 𝑧 ∧ ∀𝑥 ∈ 𝑧 ∀𝑦 ∈ 𝑧 (𝑥 ∩ 𝑦) ∈ 𝑧)} ↔ (𝐴 ⊆ (fi‘𝐴) ∧ ∀𝑥 ∈ (fi‘𝐴)∀𝑦 ∈ (fi‘𝐴)(𝑥 ∩ 𝑦) ∈ (fi‘𝐴))) |
| 51 | 41, 43, 50 | sylanblrc 590 |
. . . 4
⊢ (𝐴 ∈ V → (fi‘𝐴) ∈ {𝑧 ∣ (𝐴 ⊆ 𝑧 ∧ ∀𝑥 ∈ 𝑧 ∀𝑦 ∈ 𝑧 (𝑥 ∩ 𝑦) ∈ 𝑧)}) |
| 52 | | intss1 4963 |
. . . 4
⊢
((fi‘𝐴) ∈
{𝑧 ∣ (𝐴 ⊆ 𝑧 ∧ ∀𝑥 ∈ 𝑧 ∀𝑦 ∈ 𝑧 (𝑥 ∩ 𝑦) ∈ 𝑧)} → ∩ {𝑧 ∣ (𝐴 ⊆ 𝑧 ∧ ∀𝑥 ∈ 𝑧 ∀𝑦 ∈ 𝑧 (𝑥 ∩ 𝑦) ∈ 𝑧)} ⊆ (fi‘𝐴)) |
| 53 | 51, 52 | syl 17 |
. . 3
⊢ (𝐴 ∈ V → ∩ {𝑧
∣ (𝐴 ⊆ 𝑧 ∧ ∀𝑥 ∈ 𝑧 ∀𝑦 ∈ 𝑧 (𝑥 ∩ 𝑦) ∈ 𝑧)} ⊆ (fi‘𝐴)) |
| 54 | 40, 53 | eqssd 4001 |
. 2
⊢ (𝐴 ∈ V → (fi‘𝐴) = ∩
{𝑧 ∣ (𝐴 ⊆ 𝑧 ∧ ∀𝑥 ∈ 𝑧 ∀𝑦 ∈ 𝑧 (𝑥 ∩ 𝑦) ∈ 𝑧)}) |
| 55 | 1, 54 | syl 17 |
1
⊢ (𝐴 ∈ 𝑉 → (fi‘𝐴) = ∩ {𝑧 ∣ (𝐴 ⊆ 𝑧 ∧ ∀𝑥 ∈ 𝑧 ∀𝑦 ∈ 𝑧 (𝑥 ∩ 𝑦) ∈ 𝑧)}) |