| Step | Hyp | Ref
| Expression |
| 1 | | ovex 7464 |
. . . . . 6
⊢ (𝐽 ↾t 𝐴) ∈ V |
| 2 | | elfi2 9454 |
. . . . . 6
⊢ ((𝐽 ↾t 𝐴) ∈ V → (𝑥 ∈ (fi‘(𝐽 ↾t 𝐴)) ↔ ∃𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖
{∅})𝑥 = ∩ 𝑦)) |
| 3 | 1, 2 | ax-mp 5 |
. . . . 5
⊢ (𝑥 ∈ (fi‘(𝐽 ↾t 𝐴)) ↔ ∃𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖
{∅})𝑥 = ∩ 𝑦) |
| 4 | | eldifi 4131 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})
→ 𝑦 ∈ (𝒫
(𝐽 ↾t
𝐴) ∩
Fin)) |
| 5 | 4 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅}))
→ 𝑦 ∈ (𝒫
(𝐽 ↾t
𝐴) ∩
Fin)) |
| 6 | 5 | elin2d 4205 |
. . . . . . . . 9
⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅}))
→ 𝑦 ∈
Fin) |
| 7 | | elfpw 9394 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ (𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ↔ (𝑦 ⊆ (𝐽 ↾t 𝐴) ∧ 𝑦 ∈ Fin)) |
| 8 | 7 | simplbi 497 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ (𝒫 (𝐽 ↾t 𝐴) ∩ Fin) → 𝑦 ⊆ (𝐽 ↾t 𝐴)) |
| 9 | 5, 8 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅}))
→ 𝑦 ⊆ (𝐽 ↾t 𝐴)) |
| 10 | 9 | sseld 3982 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅}))
→ (𝑧 ∈ 𝑦 → 𝑧 ∈ (𝐽 ↾t 𝐴))) |
| 11 | | elrest 17472 |
. . . . . . . . . . . 12
⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V) → (𝑧 ∈ (𝐽 ↾t 𝐴) ↔ ∃𝑦 ∈ 𝐽 𝑧 = (𝑦 ∩ 𝐴))) |
| 12 | 11 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅}))
→ (𝑧 ∈ (𝐽 ↾t 𝐴) ↔ ∃𝑦 ∈ 𝐽 𝑧 = (𝑦 ∩ 𝐴))) |
| 13 | 10, 12 | sylibd 239 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅}))
→ (𝑧 ∈ 𝑦 → ∃𝑦 ∈ 𝐽 𝑧 = (𝑦 ∩ 𝐴))) |
| 14 | 13 | ralrimiv 3145 |
. . . . . . . . 9
⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅}))
→ ∀𝑧 ∈
𝑦 ∃𝑦 ∈ 𝐽 𝑧 = (𝑦 ∩ 𝐴)) |
| 15 | | ineq1 4213 |
. . . . . . . . . . 11
⊢ (𝑦 = (𝑓‘𝑧) → (𝑦 ∩ 𝐴) = ((𝑓‘𝑧) ∩ 𝐴)) |
| 16 | 15 | eqeq2d 2748 |
. . . . . . . . . 10
⊢ (𝑦 = (𝑓‘𝑧) → (𝑧 = (𝑦 ∩ 𝐴) ↔ 𝑧 = ((𝑓‘𝑧) ∩ 𝐴))) |
| 17 | 16 | ac6sfi 9320 |
. . . . . . . . 9
⊢ ((𝑦 ∈ Fin ∧ ∀𝑧 ∈ 𝑦 ∃𝑦 ∈ 𝐽 𝑧 = (𝑦 ∩ 𝐴)) → ∃𝑓(𝑓:𝑦⟶𝐽 ∧ ∀𝑧 ∈ 𝑦 𝑧 = ((𝑓‘𝑧) ∩ 𝐴))) |
| 18 | 6, 14, 17 | syl2anc 584 |
. . . . . . . 8
⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅}))
→ ∃𝑓(𝑓:𝑦⟶𝐽 ∧ ∀𝑧 ∈ 𝑦 𝑧 = ((𝑓‘𝑧) ∩ 𝐴))) |
| 19 | | eldifsni 4790 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})
→ 𝑦 ≠
∅) |
| 20 | 19 | ad2antlr 727 |
. . . . . . . . . . . . 13
⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅}))
∧ 𝑓:𝑦⟶𝐽) → 𝑦 ≠ ∅) |
| 21 | | iinin1 5079 |
. . . . . . . . . . . . 13
⊢ (𝑦 ≠ ∅ → ∩ 𝑧 ∈ 𝑦 ((𝑓‘𝑧) ∩ 𝐴) = (∩
𝑧 ∈ 𝑦 (𝑓‘𝑧) ∩ 𝐴)) |
| 22 | 20, 21 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅}))
∧ 𝑓:𝑦⟶𝐽) → ∩
𝑧 ∈ 𝑦 ((𝑓‘𝑧) ∩ 𝐴) = (∩
𝑧 ∈ 𝑦 (𝑓‘𝑧) ∩ 𝐴)) |
| 23 | | fvex 6919 |
. . . . . . . . . . . . 13
⊢
(fi‘𝐽) ∈
V |
| 24 | | simpllr 776 |
. . . . . . . . . . . . 13
⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅}))
∧ 𝑓:𝑦⟶𝐽) → 𝐴 ∈ V) |
| 25 | | ffn 6736 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓:𝑦⟶𝐽 → 𝑓 Fn 𝑦) |
| 26 | 25 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅}))
∧ 𝑓:𝑦⟶𝐽) → 𝑓 Fn 𝑦) |
| 27 | | fniinfv 6987 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 Fn 𝑦 → ∩
𝑧 ∈ 𝑦 (𝑓‘𝑧) = ∩ ran 𝑓) |
| 28 | 26, 27 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅}))
∧ 𝑓:𝑦⟶𝐽) → ∩
𝑧 ∈ 𝑦 (𝑓‘𝑧) = ∩ ran 𝑓) |
| 29 | | simplll 775 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅}))
∧ 𝑓:𝑦⟶𝐽) → 𝐽 ∈ V) |
| 30 | | simpr 484 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅}))
∧ 𝑓:𝑦⟶𝐽) → 𝑓:𝑦⟶𝐽) |
| 31 | 6 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅}))
∧ 𝑓:𝑦⟶𝐽) → 𝑦 ∈ Fin) |
| 32 | | intrnfi 9456 |
. . . . . . . . . . . . . . 15
⊢ ((𝐽 ∈ V ∧ (𝑓:𝑦⟶𝐽 ∧ 𝑦 ≠ ∅ ∧ 𝑦 ∈ Fin)) → ∩ ran 𝑓 ∈ (fi‘𝐽)) |
| 33 | 29, 30, 20, 31, 32 | syl13anc 1374 |
. . . . . . . . . . . . . 14
⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅}))
∧ 𝑓:𝑦⟶𝐽) → ∩ ran
𝑓 ∈ (fi‘𝐽)) |
| 34 | 28, 33 | eqeltrd 2841 |
. . . . . . . . . . . . 13
⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅}))
∧ 𝑓:𝑦⟶𝐽) → ∩
𝑧 ∈ 𝑦 (𝑓‘𝑧) ∈ (fi‘𝐽)) |
| 35 | | elrestr 17473 |
. . . . . . . . . . . . 13
⊢
(((fi‘𝐽)
∈ V ∧ 𝐴 ∈ V
∧ ∩ 𝑧 ∈ 𝑦 (𝑓‘𝑧) ∈ (fi‘𝐽)) → (∩ 𝑧 ∈ 𝑦 (𝑓‘𝑧) ∩ 𝐴) ∈ ((fi‘𝐽) ↾t 𝐴)) |
| 36 | 23, 24, 34, 35 | mp3an2i 1468 |
. . . . . . . . . . . 12
⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅}))
∧ 𝑓:𝑦⟶𝐽) → (∩ 𝑧 ∈ 𝑦 (𝑓‘𝑧) ∩ 𝐴) ∈ ((fi‘𝐽) ↾t 𝐴)) |
| 37 | 22, 36 | eqeltrd 2841 |
. . . . . . . . . . 11
⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅}))
∧ 𝑓:𝑦⟶𝐽) → ∩
𝑧 ∈ 𝑦 ((𝑓‘𝑧) ∩ 𝐴) ∈ ((fi‘𝐽) ↾t 𝐴)) |
| 38 | | intiin 5059 |
. . . . . . . . . . . . 13
⊢ ∩ 𝑦 =
∩ 𝑧 ∈ 𝑦 𝑧 |
| 39 | | iineq2 5012 |
. . . . . . . . . . . . 13
⊢
(∀𝑧 ∈
𝑦 𝑧 = ((𝑓‘𝑧) ∩ 𝐴) → ∩
𝑧 ∈ 𝑦 𝑧 = ∩ 𝑧 ∈ 𝑦 ((𝑓‘𝑧) ∩ 𝐴)) |
| 40 | 38, 39 | eqtrid 2789 |
. . . . . . . . . . . 12
⊢
(∀𝑧 ∈
𝑦 𝑧 = ((𝑓‘𝑧) ∩ 𝐴) → ∩ 𝑦 = ∩ 𝑧 ∈ 𝑦 ((𝑓‘𝑧) ∩ 𝐴)) |
| 41 | 40 | eleq1d 2826 |
. . . . . . . . . . 11
⊢
(∀𝑧 ∈
𝑦 𝑧 = ((𝑓‘𝑧) ∩ 𝐴) → (∩ 𝑦 ∈ ((fi‘𝐽) ↾t 𝐴) ↔ ∩ 𝑧 ∈ 𝑦 ((𝑓‘𝑧) ∩ 𝐴) ∈ ((fi‘𝐽) ↾t 𝐴))) |
| 42 | 37, 41 | syl5ibrcom 247 |
. . . . . . . . . 10
⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅}))
∧ 𝑓:𝑦⟶𝐽) → (∀𝑧 ∈ 𝑦 𝑧 = ((𝑓‘𝑧) ∩ 𝐴) → ∩ 𝑦 ∈ ((fi‘𝐽) ↾t 𝐴))) |
| 43 | 42 | expimpd 453 |
. . . . . . . . 9
⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅}))
→ ((𝑓:𝑦⟶𝐽 ∧ ∀𝑧 ∈ 𝑦 𝑧 = ((𝑓‘𝑧) ∩ 𝐴)) → ∩ 𝑦 ∈ ((fi‘𝐽) ↾t 𝐴))) |
| 44 | 43 | exlimdv 1933 |
. . . . . . . 8
⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅}))
→ (∃𝑓(𝑓:𝑦⟶𝐽 ∧ ∀𝑧 ∈ 𝑦 𝑧 = ((𝑓‘𝑧) ∩ 𝐴)) → ∩ 𝑦 ∈ ((fi‘𝐽) ↾t 𝐴))) |
| 45 | 18, 44 | mpd 15 |
. . . . . . 7
⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅}))
→ ∩ 𝑦 ∈ ((fi‘𝐽) ↾t 𝐴)) |
| 46 | | eleq1 2829 |
. . . . . . 7
⊢ (𝑥 = ∩
𝑦 → (𝑥 ∈ ((fi‘𝐽) ↾t 𝐴) ↔ ∩ 𝑦
∈ ((fi‘𝐽)
↾t 𝐴))) |
| 47 | 45, 46 | syl5ibrcom 247 |
. . . . . 6
⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅}))
→ (𝑥 = ∩ 𝑦
→ 𝑥 ∈
((fi‘𝐽)
↾t 𝐴))) |
| 48 | 47 | rexlimdva 3155 |
. . . . 5
⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V) → (∃𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖
{∅})𝑥 = ∩ 𝑦
→ 𝑥 ∈
((fi‘𝐽)
↾t 𝐴))) |
| 49 | 3, 48 | biimtrid 242 |
. . . 4
⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V) → (𝑥 ∈ (fi‘(𝐽 ↾t 𝐴)) → 𝑥 ∈ ((fi‘𝐽) ↾t 𝐴))) |
| 50 | | simpr 484 |
. . . . . 6
⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V) → 𝐴 ∈ V) |
| 51 | | elrest 17472 |
. . . . . 6
⊢
(((fi‘𝐽)
∈ V ∧ 𝐴 ∈ V)
→ (𝑥 ∈
((fi‘𝐽)
↾t 𝐴)
↔ ∃𝑧 ∈
(fi‘𝐽)𝑥 = (𝑧 ∩ 𝐴))) |
| 52 | 23, 50, 51 | sylancr 587 |
. . . . 5
⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V) → (𝑥 ∈ ((fi‘𝐽) ↾t 𝐴) ↔ ∃𝑧 ∈ (fi‘𝐽)𝑥 = (𝑧 ∩ 𝐴))) |
| 53 | | elfi2 9454 |
. . . . . . . 8
⊢ (𝐽 ∈ V → (𝑧 ∈ (fi‘𝐽) ↔ ∃𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖
{∅})𝑧 = ∩ 𝑦)) |
| 54 | 53 | adantr 480 |
. . . . . . 7
⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V) → (𝑧 ∈ (fi‘𝐽) ↔ ∃𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖
{∅})𝑧 = ∩ 𝑦)) |
| 55 | | eldifsni 4790 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅})
→ 𝑦 ≠
∅) |
| 56 | 55 | adantl 481 |
. . . . . . . . . . . . 13
⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅}))
→ 𝑦 ≠
∅) |
| 57 | | iinin1 5079 |
. . . . . . . . . . . . 13
⊢ (𝑦 ≠ ∅ → ∩ 𝑧 ∈ 𝑦 (𝑧 ∩ 𝐴) = (∩
𝑧 ∈ 𝑦 𝑧 ∩ 𝐴)) |
| 58 | 56, 57 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅}))
→ ∩ 𝑧 ∈ 𝑦 (𝑧 ∩ 𝐴) = (∩
𝑧 ∈ 𝑦 𝑧 ∩ 𝐴)) |
| 59 | 38 | ineq1i 4216 |
. . . . . . . . . . . 12
⊢ (∩ 𝑦
∩ 𝐴) = (∩ 𝑧 ∈ 𝑦 𝑧 ∩ 𝐴) |
| 60 | 58, 59 | eqtr4di 2795 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅}))
→ ∩ 𝑧 ∈ 𝑦 (𝑧 ∩ 𝐴) = (∩ 𝑦 ∩ 𝐴)) |
| 61 | | ovexd 7466 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅}))
→ (𝐽
↾t 𝐴)
∈ V) |
| 62 | | eldifi 4131 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅})
→ 𝑦 ∈ (𝒫
𝐽 ∩
Fin)) |
| 63 | 62 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅}))
→ 𝑦 ∈ (𝒫
𝐽 ∩
Fin)) |
| 64 | | elfpw 9394 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ (𝒫 𝐽 ∩ Fin) ↔ (𝑦 ⊆ 𝐽 ∧ 𝑦 ∈ Fin)) |
| 65 | 64 | simplbi 497 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ (𝒫 𝐽 ∩ Fin) → 𝑦 ⊆ 𝐽) |
| 66 | 63, 65 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅}))
→ 𝑦 ⊆ 𝐽) |
| 67 | | elrestr 17473 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V ∧ 𝑧 ∈ 𝐽) → (𝑧 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴)) |
| 68 | 67 | 3expa 1119 |
. . . . . . . . . . . . . . 15
⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑧 ∈ 𝐽) → (𝑧 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴)) |
| 69 | 68 | ralrimiva 3146 |
. . . . . . . . . . . . . 14
⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V) → ∀𝑧 ∈ 𝐽 (𝑧 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴)) |
| 70 | 69 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅}))
→ ∀𝑧 ∈
𝐽 (𝑧 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴)) |
| 71 | | ssralv 4052 |
. . . . . . . . . . . . 13
⊢ (𝑦 ⊆ 𝐽 → (∀𝑧 ∈ 𝐽 (𝑧 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴) → ∀𝑧 ∈ 𝑦 (𝑧 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴))) |
| 72 | 66, 70, 71 | sylc 65 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅}))
→ ∀𝑧 ∈
𝑦 (𝑧 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴)) |
| 73 | 63 | elin2d 4205 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅}))
→ 𝑦 ∈
Fin) |
| 74 | | iinfi 9457 |
. . . . . . . . . . . 12
⊢ (((𝐽 ↾t 𝐴) ∈ V ∧ (∀𝑧 ∈ 𝑦 (𝑧 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴) ∧ 𝑦 ≠ ∅ ∧ 𝑦 ∈ Fin)) → ∩ 𝑧 ∈ 𝑦 (𝑧 ∩ 𝐴) ∈ (fi‘(𝐽 ↾t 𝐴))) |
| 75 | 61, 72, 56, 73, 74 | syl13anc 1374 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅}))
→ ∩ 𝑧 ∈ 𝑦 (𝑧 ∩ 𝐴) ∈ (fi‘(𝐽 ↾t 𝐴))) |
| 76 | 60, 75 | eqeltrrd 2842 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅}))
→ (∩ 𝑦 ∩ 𝐴) ∈ (fi‘(𝐽 ↾t 𝐴))) |
| 77 | | eleq1 2829 |
. . . . . . . . . 10
⊢ (𝑥 = (∩
𝑦 ∩ 𝐴) → (𝑥 ∈ (fi‘(𝐽 ↾t 𝐴)) ↔ (∩
𝑦 ∩ 𝐴) ∈ (fi‘(𝐽 ↾t 𝐴)))) |
| 78 | 76, 77 | syl5ibrcom 247 |
. . . . . . . . 9
⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅}))
→ (𝑥 = (∩ 𝑦
∩ 𝐴) → 𝑥 ∈ (fi‘(𝐽 ↾t 𝐴)))) |
| 79 | | ineq1 4213 |
. . . . . . . . . . 11
⊢ (𝑧 = ∩
𝑦 → (𝑧 ∩ 𝐴) = (∩ 𝑦 ∩ 𝐴)) |
| 80 | 79 | eqeq2d 2748 |
. . . . . . . . . 10
⊢ (𝑧 = ∩
𝑦 → (𝑥 = (𝑧 ∩ 𝐴) ↔ 𝑥 = (∩ 𝑦 ∩ 𝐴))) |
| 81 | 80 | imbi1d 341 |
. . . . . . . . 9
⊢ (𝑧 = ∩
𝑦 → ((𝑥 = (𝑧 ∩ 𝐴) → 𝑥 ∈ (fi‘(𝐽 ↾t 𝐴))) ↔ (𝑥 = (∩ 𝑦 ∩ 𝐴) → 𝑥 ∈ (fi‘(𝐽 ↾t 𝐴))))) |
| 82 | 78, 81 | syl5ibrcom 247 |
. . . . . . . 8
⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅}))
→ (𝑧 = ∩ 𝑦
→ (𝑥 = (𝑧 ∩ 𝐴) → 𝑥 ∈ (fi‘(𝐽 ↾t 𝐴))))) |
| 83 | 82 | rexlimdva 3155 |
. . . . . . 7
⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V) → (∃𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖
{∅})𝑧 = ∩ 𝑦
→ (𝑥 = (𝑧 ∩ 𝐴) → 𝑥 ∈ (fi‘(𝐽 ↾t 𝐴))))) |
| 84 | 54, 83 | sylbid 240 |
. . . . . 6
⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V) → (𝑧 ∈ (fi‘𝐽) → (𝑥 = (𝑧 ∩ 𝐴) → 𝑥 ∈ (fi‘(𝐽 ↾t 𝐴))))) |
| 85 | 84 | rexlimdv 3153 |
. . . . 5
⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V) → (∃𝑧 ∈ (fi‘𝐽)𝑥 = (𝑧 ∩ 𝐴) → 𝑥 ∈ (fi‘(𝐽 ↾t 𝐴)))) |
| 86 | 52, 85 | sylbid 240 |
. . . 4
⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V) → (𝑥 ∈ ((fi‘𝐽) ↾t 𝐴) → 𝑥 ∈ (fi‘(𝐽 ↾t 𝐴)))) |
| 87 | 49, 86 | impbid 212 |
. . 3
⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V) → (𝑥 ∈ (fi‘(𝐽 ↾t 𝐴)) ↔ 𝑥 ∈ ((fi‘𝐽) ↾t 𝐴))) |
| 88 | 87 | eqrdv 2735 |
. 2
⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V) →
(fi‘(𝐽
↾t 𝐴)) =
((fi‘𝐽)
↾t 𝐴)) |
| 89 | | fi0 9460 |
. . 3
⊢
(fi‘∅) = ∅ |
| 90 | | relxp 5703 |
. . . . . 6
⊢ Rel (V
× V) |
| 91 | | restfn 17469 |
. . . . . . . 8
⊢
↾t Fn (V × V) |
| 92 | 91 | fndmi 6672 |
. . . . . . 7
⊢ dom
↾t = (V × V) |
| 93 | 92 | releqi 5787 |
. . . . . 6
⊢ (Rel dom
↾t ↔ Rel (V × V)) |
| 94 | 90, 93 | mpbir 231 |
. . . . 5
⊢ Rel dom
↾t |
| 95 | 94 | ovprc 7469 |
. . . 4
⊢ (¬
(𝐽 ∈ V ∧ 𝐴 ∈ V) → (𝐽 ↾t 𝐴) = ∅) |
| 96 | 95 | fveq2d 6910 |
. . 3
⊢ (¬
(𝐽 ∈ V ∧ 𝐴 ∈ V) →
(fi‘(𝐽
↾t 𝐴)) =
(fi‘∅)) |
| 97 | | ianor 984 |
. . . 4
⊢ (¬
(𝐽 ∈ V ∧ 𝐴 ∈ V) ↔ (¬ 𝐽 ∈ V ∨ ¬ 𝐴 ∈ V)) |
| 98 | | fvprc 6898 |
. . . . . . 7
⊢ (¬
𝐽 ∈ V →
(fi‘𝐽) =
∅) |
| 99 | 98 | oveq1d 7446 |
. . . . . 6
⊢ (¬
𝐽 ∈ V →
((fi‘𝐽)
↾t 𝐴) =
(∅ ↾t 𝐴)) |
| 100 | | 0rest 17474 |
. . . . . 6
⊢ (∅
↾t 𝐴) =
∅ |
| 101 | 99, 100 | eqtrdi 2793 |
. . . . 5
⊢ (¬
𝐽 ∈ V →
((fi‘𝐽)
↾t 𝐴) =
∅) |
| 102 | 94 | ovprc2 7471 |
. . . . 5
⊢ (¬
𝐴 ∈ V →
((fi‘𝐽)
↾t 𝐴) =
∅) |
| 103 | 101, 102 | jaoi 858 |
. . . 4
⊢ ((¬
𝐽 ∈ V ∨ ¬ 𝐴 ∈ V) →
((fi‘𝐽)
↾t 𝐴) =
∅) |
| 104 | 97, 103 | sylbi 217 |
. . 3
⊢ (¬
(𝐽 ∈ V ∧ 𝐴 ∈ V) →
((fi‘𝐽)
↾t 𝐴) =
∅) |
| 105 | 89, 96, 104 | 3eqtr4a 2803 |
. 2
⊢ (¬
(𝐽 ∈ V ∧ 𝐴 ∈ V) →
(fi‘(𝐽
↾t 𝐴)) =
((fi‘𝐽)
↾t 𝐴)) |
| 106 | 88, 105 | pm2.61i 182 |
1
⊢
(fi‘(𝐽
↾t 𝐴)) =
((fi‘𝐽)
↾t 𝐴) |