Step | Hyp | Ref
| Expression |
1 | | ovex 7183 |
. . . . . 6
⊢ (𝐽 ↾t 𝐴) ∈ V |
2 | | elfi2 8872 |
. . . . . 6
⊢ ((𝐽 ↾t 𝐴) ∈ V → (𝑥 ∈ (fi‘(𝐽 ↾t 𝐴)) ↔ ∃𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖
{∅})𝑥 = ∩ 𝑦)) |
3 | 1, 2 | ax-mp 5 |
. . . . 5
⊢ (𝑥 ∈ (fi‘(𝐽 ↾t 𝐴)) ↔ ∃𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖
{∅})𝑥 = ∩ 𝑦) |
4 | | eldifi 4102 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})
→ 𝑦 ∈ (𝒫
(𝐽 ↾t
𝐴) ∩
Fin)) |
5 | 4 | adantl 484 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅}))
→ 𝑦 ∈ (𝒫
(𝐽 ↾t
𝐴) ∩
Fin)) |
6 | 5 | elin2d 4175 |
. . . . . . . . 9
⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅}))
→ 𝑦 ∈
Fin) |
7 | | elfpw 8820 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ (𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ↔ (𝑦 ⊆ (𝐽 ↾t 𝐴) ∧ 𝑦 ∈ Fin)) |
8 | 7 | simplbi 500 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ (𝒫 (𝐽 ↾t 𝐴) ∩ Fin) → 𝑦 ⊆ (𝐽 ↾t 𝐴)) |
9 | 5, 8 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅}))
→ 𝑦 ⊆ (𝐽 ↾t 𝐴)) |
10 | 9 | sseld 3965 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅}))
→ (𝑧 ∈ 𝑦 → 𝑧 ∈ (𝐽 ↾t 𝐴))) |
11 | | elrest 16695 |
. . . . . . . . . . . 12
⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V) → (𝑧 ∈ (𝐽 ↾t 𝐴) ↔ ∃𝑦 ∈ 𝐽 𝑧 = (𝑦 ∩ 𝐴))) |
12 | 11 | adantr 483 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅}))
→ (𝑧 ∈ (𝐽 ↾t 𝐴) ↔ ∃𝑦 ∈ 𝐽 𝑧 = (𝑦 ∩ 𝐴))) |
13 | 10, 12 | sylibd 241 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅}))
→ (𝑧 ∈ 𝑦 → ∃𝑦 ∈ 𝐽 𝑧 = (𝑦 ∩ 𝐴))) |
14 | 13 | ralrimiv 3181 |
. . . . . . . . 9
⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅}))
→ ∀𝑧 ∈
𝑦 ∃𝑦 ∈ 𝐽 𝑧 = (𝑦 ∩ 𝐴)) |
15 | | ineq1 4180 |
. . . . . . . . . . 11
⊢ (𝑦 = (𝑓‘𝑧) → (𝑦 ∩ 𝐴) = ((𝑓‘𝑧) ∩ 𝐴)) |
16 | 15 | eqeq2d 2832 |
. . . . . . . . . 10
⊢ (𝑦 = (𝑓‘𝑧) → (𝑧 = (𝑦 ∩ 𝐴) ↔ 𝑧 = ((𝑓‘𝑧) ∩ 𝐴))) |
17 | 16 | ac6sfi 8756 |
. . . . . . . . 9
⊢ ((𝑦 ∈ Fin ∧ ∀𝑧 ∈ 𝑦 ∃𝑦 ∈ 𝐽 𝑧 = (𝑦 ∩ 𝐴)) → ∃𝑓(𝑓:𝑦⟶𝐽 ∧ ∀𝑧 ∈ 𝑦 𝑧 = ((𝑓‘𝑧) ∩ 𝐴))) |
18 | 6, 14, 17 | syl2anc 586 |
. . . . . . . 8
⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅}))
→ ∃𝑓(𝑓:𝑦⟶𝐽 ∧ ∀𝑧 ∈ 𝑦 𝑧 = ((𝑓‘𝑧) ∩ 𝐴))) |
19 | | eldifsni 4715 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})
→ 𝑦 ≠
∅) |
20 | 19 | ad2antlr 725 |
. . . . . . . . . . . . 13
⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅}))
∧ 𝑓:𝑦⟶𝐽) → 𝑦 ≠ ∅) |
21 | | iinin1 4993 |
. . . . . . . . . . . . 13
⊢ (𝑦 ≠ ∅ → ∩ 𝑧 ∈ 𝑦 ((𝑓‘𝑧) ∩ 𝐴) = (∩
𝑧 ∈ 𝑦 (𝑓‘𝑧) ∩ 𝐴)) |
22 | 20, 21 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅}))
∧ 𝑓:𝑦⟶𝐽) → ∩
𝑧 ∈ 𝑦 ((𝑓‘𝑧) ∩ 𝐴) = (∩
𝑧 ∈ 𝑦 (𝑓‘𝑧) ∩ 𝐴)) |
23 | | fvex 6677 |
. . . . . . . . . . . . 13
⊢
(fi‘𝐽) ∈
V |
24 | | simpllr 774 |
. . . . . . . . . . . . 13
⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅}))
∧ 𝑓:𝑦⟶𝐽) → 𝐴 ∈ V) |
25 | | ffn 6508 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓:𝑦⟶𝐽 → 𝑓 Fn 𝑦) |
26 | 25 | adantl 484 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅}))
∧ 𝑓:𝑦⟶𝐽) → 𝑓 Fn 𝑦) |
27 | | fniinfv 6736 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 Fn 𝑦 → ∩
𝑧 ∈ 𝑦 (𝑓‘𝑧) = ∩ ran 𝑓) |
28 | 26, 27 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅}))
∧ 𝑓:𝑦⟶𝐽) → ∩
𝑧 ∈ 𝑦 (𝑓‘𝑧) = ∩ ran 𝑓) |
29 | | simplll 773 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅}))
∧ 𝑓:𝑦⟶𝐽) → 𝐽 ∈ V) |
30 | | simpr 487 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅}))
∧ 𝑓:𝑦⟶𝐽) → 𝑓:𝑦⟶𝐽) |
31 | 6 | adantr 483 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅}))
∧ 𝑓:𝑦⟶𝐽) → 𝑦 ∈ Fin) |
32 | | intrnfi 8874 |
. . . . . . . . . . . . . . 15
⊢ ((𝐽 ∈ V ∧ (𝑓:𝑦⟶𝐽 ∧ 𝑦 ≠ ∅ ∧ 𝑦 ∈ Fin)) → ∩ ran 𝑓 ∈ (fi‘𝐽)) |
33 | 29, 30, 20, 31, 32 | syl13anc 1368 |
. . . . . . . . . . . . . 14
⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅}))
∧ 𝑓:𝑦⟶𝐽) → ∩ ran
𝑓 ∈ (fi‘𝐽)) |
34 | 28, 33 | eqeltrd 2913 |
. . . . . . . . . . . . 13
⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅}))
∧ 𝑓:𝑦⟶𝐽) → ∩
𝑧 ∈ 𝑦 (𝑓‘𝑧) ∈ (fi‘𝐽)) |
35 | | elrestr 16696 |
. . . . . . . . . . . . 13
⊢
(((fi‘𝐽)
∈ V ∧ 𝐴 ∈ V
∧ ∩ 𝑧 ∈ 𝑦 (𝑓‘𝑧) ∈ (fi‘𝐽)) → (∩ 𝑧 ∈ 𝑦 (𝑓‘𝑧) ∩ 𝐴) ∈ ((fi‘𝐽) ↾t 𝐴)) |
36 | 23, 24, 34, 35 | mp3an2i 1462 |
. . . . . . . . . . . 12
⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅}))
∧ 𝑓:𝑦⟶𝐽) → (∩ 𝑧 ∈ 𝑦 (𝑓‘𝑧) ∩ 𝐴) ∈ ((fi‘𝐽) ↾t 𝐴)) |
37 | 22, 36 | eqeltrd 2913 |
. . . . . . . . . . 11
⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅}))
∧ 𝑓:𝑦⟶𝐽) → ∩
𝑧 ∈ 𝑦 ((𝑓‘𝑧) ∩ 𝐴) ∈ ((fi‘𝐽) ↾t 𝐴)) |
38 | | intiin 4975 |
. . . . . . . . . . . . 13
⊢ ∩ 𝑦 =
∩ 𝑧 ∈ 𝑦 𝑧 |
39 | | iineq2 4931 |
. . . . . . . . . . . . 13
⊢
(∀𝑧 ∈
𝑦 𝑧 = ((𝑓‘𝑧) ∩ 𝐴) → ∩
𝑧 ∈ 𝑦 𝑧 = ∩ 𝑧 ∈ 𝑦 ((𝑓‘𝑧) ∩ 𝐴)) |
40 | 38, 39 | syl5eq 2868 |
. . . . . . . . . . . 12
⊢
(∀𝑧 ∈
𝑦 𝑧 = ((𝑓‘𝑧) ∩ 𝐴) → ∩ 𝑦 = ∩ 𝑧 ∈ 𝑦 ((𝑓‘𝑧) ∩ 𝐴)) |
41 | 40 | eleq1d 2897 |
. . . . . . . . . . 11
⊢
(∀𝑧 ∈
𝑦 𝑧 = ((𝑓‘𝑧) ∩ 𝐴) → (∩ 𝑦 ∈ ((fi‘𝐽) ↾t 𝐴) ↔ ∩ 𝑧 ∈ 𝑦 ((𝑓‘𝑧) ∩ 𝐴) ∈ ((fi‘𝐽) ↾t 𝐴))) |
42 | 37, 41 | syl5ibrcom 249 |
. . . . . . . . . 10
⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅}))
∧ 𝑓:𝑦⟶𝐽) → (∀𝑧 ∈ 𝑦 𝑧 = ((𝑓‘𝑧) ∩ 𝐴) → ∩ 𝑦 ∈ ((fi‘𝐽) ↾t 𝐴))) |
43 | 42 | expimpd 456 |
. . . . . . . . 9
⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅}))
→ ((𝑓:𝑦⟶𝐽 ∧ ∀𝑧 ∈ 𝑦 𝑧 = ((𝑓‘𝑧) ∩ 𝐴)) → ∩ 𝑦 ∈ ((fi‘𝐽) ↾t 𝐴))) |
44 | 43 | exlimdv 1930 |
. . . . . . . 8
⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅}))
→ (∃𝑓(𝑓:𝑦⟶𝐽 ∧ ∀𝑧 ∈ 𝑦 𝑧 = ((𝑓‘𝑧) ∩ 𝐴)) → ∩ 𝑦 ∈ ((fi‘𝐽) ↾t 𝐴))) |
45 | 18, 44 | mpd 15 |
. . . . . . 7
⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅}))
→ ∩ 𝑦 ∈ ((fi‘𝐽) ↾t 𝐴)) |
46 | | eleq1 2900 |
. . . . . . 7
⊢ (𝑥 = ∩
𝑦 → (𝑥 ∈ ((fi‘𝐽) ↾t 𝐴) ↔ ∩ 𝑦
∈ ((fi‘𝐽)
↾t 𝐴))) |
47 | 45, 46 | syl5ibrcom 249 |
. . . . . 6
⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅}))
→ (𝑥 = ∩ 𝑦
→ 𝑥 ∈
((fi‘𝐽)
↾t 𝐴))) |
48 | 47 | rexlimdva 3284 |
. . . . 5
⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V) → (∃𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖
{∅})𝑥 = ∩ 𝑦
→ 𝑥 ∈
((fi‘𝐽)
↾t 𝐴))) |
49 | 3, 48 | syl5bi 244 |
. . . 4
⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V) → (𝑥 ∈ (fi‘(𝐽 ↾t 𝐴)) → 𝑥 ∈ ((fi‘𝐽) ↾t 𝐴))) |
50 | | simpr 487 |
. . . . . 6
⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V) → 𝐴 ∈ V) |
51 | | elrest 16695 |
. . . . . 6
⊢
(((fi‘𝐽)
∈ V ∧ 𝐴 ∈ V)
→ (𝑥 ∈
((fi‘𝐽)
↾t 𝐴)
↔ ∃𝑧 ∈
(fi‘𝐽)𝑥 = (𝑧 ∩ 𝐴))) |
52 | 23, 50, 51 | sylancr 589 |
. . . . 5
⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V) → (𝑥 ∈ ((fi‘𝐽) ↾t 𝐴) ↔ ∃𝑧 ∈ (fi‘𝐽)𝑥 = (𝑧 ∩ 𝐴))) |
53 | | elfi2 8872 |
. . . . . . . 8
⊢ (𝐽 ∈ V → (𝑧 ∈ (fi‘𝐽) ↔ ∃𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖
{∅})𝑧 = ∩ 𝑦)) |
54 | 53 | adantr 483 |
. . . . . . 7
⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V) → (𝑧 ∈ (fi‘𝐽) ↔ ∃𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖
{∅})𝑧 = ∩ 𝑦)) |
55 | | eldifsni 4715 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅})
→ 𝑦 ≠
∅) |
56 | 55 | adantl 484 |
. . . . . . . . . . . . 13
⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅}))
→ 𝑦 ≠
∅) |
57 | | iinin1 4993 |
. . . . . . . . . . . . 13
⊢ (𝑦 ≠ ∅ → ∩ 𝑧 ∈ 𝑦 (𝑧 ∩ 𝐴) = (∩
𝑧 ∈ 𝑦 𝑧 ∩ 𝐴)) |
58 | 56, 57 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅}))
→ ∩ 𝑧 ∈ 𝑦 (𝑧 ∩ 𝐴) = (∩
𝑧 ∈ 𝑦 𝑧 ∩ 𝐴)) |
59 | 38 | ineq1i 4184 |
. . . . . . . . . . . 12
⊢ (∩ 𝑦
∩ 𝐴) = (∩ 𝑧 ∈ 𝑦 𝑧 ∩ 𝐴) |
60 | 58, 59 | syl6eqr 2874 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅}))
→ ∩ 𝑧 ∈ 𝑦 (𝑧 ∩ 𝐴) = (∩ 𝑦 ∩ 𝐴)) |
61 | | ovexd 7185 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅}))
→ (𝐽
↾t 𝐴)
∈ V) |
62 | | eldifi 4102 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅})
→ 𝑦 ∈ (𝒫
𝐽 ∩
Fin)) |
63 | 62 | adantl 484 |
. . . . . . . . . . . . . 14
⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅}))
→ 𝑦 ∈ (𝒫
𝐽 ∩
Fin)) |
64 | | elfpw 8820 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ (𝒫 𝐽 ∩ Fin) ↔ (𝑦 ⊆ 𝐽 ∧ 𝑦 ∈ Fin)) |
65 | 64 | simplbi 500 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ (𝒫 𝐽 ∩ Fin) → 𝑦 ⊆ 𝐽) |
66 | 63, 65 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅}))
→ 𝑦 ⊆ 𝐽) |
67 | | elrestr 16696 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V ∧ 𝑧 ∈ 𝐽) → (𝑧 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴)) |
68 | 67 | 3expa 1114 |
. . . . . . . . . . . . . . 15
⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑧 ∈ 𝐽) → (𝑧 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴)) |
69 | 68 | ralrimiva 3182 |
. . . . . . . . . . . . . 14
⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V) → ∀𝑧 ∈ 𝐽 (𝑧 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴)) |
70 | 69 | adantr 483 |
. . . . . . . . . . . . 13
⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅}))
→ ∀𝑧 ∈
𝐽 (𝑧 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴)) |
71 | | ssralv 4032 |
. . . . . . . . . . . . 13
⊢ (𝑦 ⊆ 𝐽 → (∀𝑧 ∈ 𝐽 (𝑧 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴) → ∀𝑧 ∈ 𝑦 (𝑧 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴))) |
72 | 66, 70, 71 | sylc 65 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅}))
→ ∀𝑧 ∈
𝑦 (𝑧 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴)) |
73 | 63 | elin2d 4175 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅}))
→ 𝑦 ∈
Fin) |
74 | | iinfi 8875 |
. . . . . . . . . . . 12
⊢ (((𝐽 ↾t 𝐴) ∈ V ∧ (∀𝑧 ∈ 𝑦 (𝑧 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴) ∧ 𝑦 ≠ ∅ ∧ 𝑦 ∈ Fin)) → ∩ 𝑧 ∈ 𝑦 (𝑧 ∩ 𝐴) ∈ (fi‘(𝐽 ↾t 𝐴))) |
75 | 61, 72, 56, 73, 74 | syl13anc 1368 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅}))
→ ∩ 𝑧 ∈ 𝑦 (𝑧 ∩ 𝐴) ∈ (fi‘(𝐽 ↾t 𝐴))) |
76 | 60, 75 | eqeltrrd 2914 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅}))
→ (∩ 𝑦 ∩ 𝐴) ∈ (fi‘(𝐽 ↾t 𝐴))) |
77 | | eleq1 2900 |
. . . . . . . . . 10
⊢ (𝑥 = (∩
𝑦 ∩ 𝐴) → (𝑥 ∈ (fi‘(𝐽 ↾t 𝐴)) ↔ (∩
𝑦 ∩ 𝐴) ∈ (fi‘(𝐽 ↾t 𝐴)))) |
78 | 76, 77 | syl5ibrcom 249 |
. . . . . . . . 9
⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅}))
→ (𝑥 = (∩ 𝑦
∩ 𝐴) → 𝑥 ∈ (fi‘(𝐽 ↾t 𝐴)))) |
79 | | ineq1 4180 |
. . . . . . . . . . 11
⊢ (𝑧 = ∩
𝑦 → (𝑧 ∩ 𝐴) = (∩ 𝑦 ∩ 𝐴)) |
80 | 79 | eqeq2d 2832 |
. . . . . . . . . 10
⊢ (𝑧 = ∩
𝑦 → (𝑥 = (𝑧 ∩ 𝐴) ↔ 𝑥 = (∩ 𝑦 ∩ 𝐴))) |
81 | 80 | imbi1d 344 |
. . . . . . . . 9
⊢ (𝑧 = ∩
𝑦 → ((𝑥 = (𝑧 ∩ 𝐴) → 𝑥 ∈ (fi‘(𝐽 ↾t 𝐴))) ↔ (𝑥 = (∩ 𝑦 ∩ 𝐴) → 𝑥 ∈ (fi‘(𝐽 ↾t 𝐴))))) |
82 | 78, 81 | syl5ibrcom 249 |
. . . . . . . 8
⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅}))
→ (𝑧 = ∩ 𝑦
→ (𝑥 = (𝑧 ∩ 𝐴) → 𝑥 ∈ (fi‘(𝐽 ↾t 𝐴))))) |
83 | 82 | rexlimdva 3284 |
. . . . . . 7
⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V) → (∃𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖
{∅})𝑧 = ∩ 𝑦
→ (𝑥 = (𝑧 ∩ 𝐴) → 𝑥 ∈ (fi‘(𝐽 ↾t 𝐴))))) |
84 | 54, 83 | sylbid 242 |
. . . . . 6
⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V) → (𝑧 ∈ (fi‘𝐽) → (𝑥 = (𝑧 ∩ 𝐴) → 𝑥 ∈ (fi‘(𝐽 ↾t 𝐴))))) |
85 | 84 | rexlimdv 3283 |
. . . . 5
⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V) → (∃𝑧 ∈ (fi‘𝐽)𝑥 = (𝑧 ∩ 𝐴) → 𝑥 ∈ (fi‘(𝐽 ↾t 𝐴)))) |
86 | 52, 85 | sylbid 242 |
. . . 4
⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V) → (𝑥 ∈ ((fi‘𝐽) ↾t 𝐴) → 𝑥 ∈ (fi‘(𝐽 ↾t 𝐴)))) |
87 | 49, 86 | impbid 214 |
. . 3
⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V) → (𝑥 ∈ (fi‘(𝐽 ↾t 𝐴)) ↔ 𝑥 ∈ ((fi‘𝐽) ↾t 𝐴))) |
88 | 87 | eqrdv 2819 |
. 2
⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V) →
(fi‘(𝐽
↾t 𝐴)) =
((fi‘𝐽)
↾t 𝐴)) |
89 | | fi0 8878 |
. . 3
⊢
(fi‘∅) = ∅ |
90 | | relxp 5567 |
. . . . . 6
⊢ Rel (V
× V) |
91 | | restfn 16692 |
. . . . . . . 8
⊢
↾t Fn (V × V) |
92 | | fndm 6449 |
. . . . . . . 8
⊢ (
↾t Fn (V × V) → dom ↾t = (V
× V)) |
93 | 91, 92 | ax-mp 5 |
. . . . . . 7
⊢ dom
↾t = (V × V) |
94 | 93 | releqi 5646 |
. . . . . 6
⊢ (Rel dom
↾t ↔ Rel (V × V)) |
95 | 90, 94 | mpbir 233 |
. . . . 5
⊢ Rel dom
↾t |
96 | 95 | ovprc 7188 |
. . . 4
⊢ (¬
(𝐽 ∈ V ∧ 𝐴 ∈ V) → (𝐽 ↾t 𝐴) = ∅) |
97 | 96 | fveq2d 6668 |
. . 3
⊢ (¬
(𝐽 ∈ V ∧ 𝐴 ∈ V) →
(fi‘(𝐽
↾t 𝐴)) =
(fi‘∅)) |
98 | | ianor 978 |
. . . 4
⊢ (¬
(𝐽 ∈ V ∧ 𝐴 ∈ V) ↔ (¬ 𝐽 ∈ V ∨ ¬ 𝐴 ∈ V)) |
99 | | fvprc 6657 |
. . . . . . 7
⊢ (¬
𝐽 ∈ V →
(fi‘𝐽) =
∅) |
100 | 99 | oveq1d 7165 |
. . . . . 6
⊢ (¬
𝐽 ∈ V →
((fi‘𝐽)
↾t 𝐴) =
(∅ ↾t 𝐴)) |
101 | | 0rest 16697 |
. . . . . 6
⊢ (∅
↾t 𝐴) =
∅ |
102 | 100, 101 | syl6eq 2872 |
. . . . 5
⊢ (¬
𝐽 ∈ V →
((fi‘𝐽)
↾t 𝐴) =
∅) |
103 | 95 | ovprc2 7190 |
. . . . 5
⊢ (¬
𝐴 ∈ V →
((fi‘𝐽)
↾t 𝐴) =
∅) |
104 | 102, 103 | jaoi 853 |
. . . 4
⊢ ((¬
𝐽 ∈ V ∨ ¬ 𝐴 ∈ V) →
((fi‘𝐽)
↾t 𝐴) =
∅) |
105 | 98, 104 | sylbi 219 |
. . 3
⊢ (¬
(𝐽 ∈ V ∧ 𝐴 ∈ V) →
((fi‘𝐽)
↾t 𝐴) =
∅) |
106 | 89, 97, 105 | 3eqtr4a 2882 |
. 2
⊢ (¬
(𝐽 ∈ V ∧ 𝐴 ∈ V) →
(fi‘(𝐽
↾t 𝐴)) =
((fi‘𝐽)
↾t 𝐴)) |
107 | 88, 106 | pm2.61i 184 |
1
⊢
(fi‘(𝐽
↾t 𝐴)) =
((fi‘𝐽)
↾t 𝐴) |