Step | Hyp | Ref
| Expression |
1 | | ovex 6678 |
. . . . . 6
⊢ (𝐽 ↾t 𝐴) ∈ V |
2 | | elfi2 8320 |
. . . . . 6
⊢ ((𝐽 ↾t 𝐴) ∈ V → (𝑥 ∈ (fi‘(𝐽 ↾t 𝐴)) ↔ ∃𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖
{∅})𝑥 = ∩ 𝑦)) |
3 | 1, 2 | ax-mp 5 |
. . . . 5
⊢ (𝑥 ∈ (fi‘(𝐽 ↾t 𝐴)) ↔ ∃𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖
{∅})𝑥 = ∩ 𝑦) |
4 | | eldifi 3732 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})
→ 𝑦 ∈ (𝒫
(𝐽 ↾t
𝐴) ∩
Fin)) |
5 | 4 | adantl 482 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅}))
→ 𝑦 ∈ (𝒫
(𝐽 ↾t
𝐴) ∩
Fin)) |
6 | | elfpw 8268 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ (𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ↔ (𝑦 ⊆ (𝐽 ↾t 𝐴) ∧ 𝑦 ∈ Fin)) |
7 | 6 | simprbi 480 |
. . . . . . . . . 10
⊢ (𝑦 ∈ (𝒫 (𝐽 ↾t 𝐴) ∩ Fin) → 𝑦 ∈ Fin) |
8 | 5, 7 | syl 17 |
. . . . . . . . 9
⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅}))
→ 𝑦 ∈
Fin) |
9 | 6 | simplbi 476 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ (𝒫 (𝐽 ↾t 𝐴) ∩ Fin) → 𝑦 ⊆ (𝐽 ↾t 𝐴)) |
10 | 5, 9 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅}))
→ 𝑦 ⊆ (𝐽 ↾t 𝐴)) |
11 | 10 | sseld 3602 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅}))
→ (𝑧 ∈ 𝑦 → 𝑧 ∈ (𝐽 ↾t 𝐴))) |
12 | | elrest 16088 |
. . . . . . . . . . . 12
⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V) → (𝑧 ∈ (𝐽 ↾t 𝐴) ↔ ∃𝑦 ∈ 𝐽 𝑧 = (𝑦 ∩ 𝐴))) |
13 | 12 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅}))
→ (𝑧 ∈ (𝐽 ↾t 𝐴) ↔ ∃𝑦 ∈ 𝐽 𝑧 = (𝑦 ∩ 𝐴))) |
14 | 11, 13 | sylibd 229 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅}))
→ (𝑧 ∈ 𝑦 → ∃𝑦 ∈ 𝐽 𝑧 = (𝑦 ∩ 𝐴))) |
15 | 14 | ralrimiv 2965 |
. . . . . . . . 9
⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅}))
→ ∀𝑧 ∈
𝑦 ∃𝑦 ∈ 𝐽 𝑧 = (𝑦 ∩ 𝐴)) |
16 | | ineq1 3807 |
. . . . . . . . . . 11
⊢ (𝑦 = (𝑓‘𝑧) → (𝑦 ∩ 𝐴) = ((𝑓‘𝑧) ∩ 𝐴)) |
17 | 16 | eqeq2d 2632 |
. . . . . . . . . 10
⊢ (𝑦 = (𝑓‘𝑧) → (𝑧 = (𝑦 ∩ 𝐴) ↔ 𝑧 = ((𝑓‘𝑧) ∩ 𝐴))) |
18 | 17 | ac6sfi 8204 |
. . . . . . . . 9
⊢ ((𝑦 ∈ Fin ∧ ∀𝑧 ∈ 𝑦 ∃𝑦 ∈ 𝐽 𝑧 = (𝑦 ∩ 𝐴)) → ∃𝑓(𝑓:𝑦⟶𝐽 ∧ ∀𝑧 ∈ 𝑦 𝑧 = ((𝑓‘𝑧) ∩ 𝐴))) |
19 | 8, 15, 18 | syl2anc 693 |
. . . . . . . 8
⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅}))
→ ∃𝑓(𝑓:𝑦⟶𝐽 ∧ ∀𝑧 ∈ 𝑦 𝑧 = ((𝑓‘𝑧) ∩ 𝐴))) |
20 | | eldifsni 4320 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅})
→ 𝑦 ≠
∅) |
21 | 20 | ad2antlr 763 |
. . . . . . . . . . . . 13
⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅}))
∧ 𝑓:𝑦⟶𝐽) → 𝑦 ≠ ∅) |
22 | | iinin1 4591 |
. . . . . . . . . . . . 13
⊢ (𝑦 ≠ ∅ → ∩ 𝑧 ∈ 𝑦 ((𝑓‘𝑧) ∩ 𝐴) = (∩
𝑧 ∈ 𝑦 (𝑓‘𝑧) ∩ 𝐴)) |
23 | 21, 22 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅}))
∧ 𝑓:𝑦⟶𝐽) → ∩
𝑧 ∈ 𝑦 ((𝑓‘𝑧) ∩ 𝐴) = (∩
𝑧 ∈ 𝑦 (𝑓‘𝑧) ∩ 𝐴)) |
24 | | fvex 6201 |
. . . . . . . . . . . . . 14
⊢
(fi‘𝐽) ∈
V |
25 | 24 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅}))
∧ 𝑓:𝑦⟶𝐽) → (fi‘𝐽) ∈ V) |
26 | | simpllr 799 |
. . . . . . . . . . . . 13
⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅}))
∧ 𝑓:𝑦⟶𝐽) → 𝐴 ∈ V) |
27 | | ffn 6045 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓:𝑦⟶𝐽 → 𝑓 Fn 𝑦) |
28 | 27 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅}))
∧ 𝑓:𝑦⟶𝐽) → 𝑓 Fn 𝑦) |
29 | | fniinfv 6257 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 Fn 𝑦 → ∩
𝑧 ∈ 𝑦 (𝑓‘𝑧) = ∩ ran 𝑓) |
30 | 28, 29 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅}))
∧ 𝑓:𝑦⟶𝐽) → ∩
𝑧 ∈ 𝑦 (𝑓‘𝑧) = ∩ ran 𝑓) |
31 | | simplll 798 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅}))
∧ 𝑓:𝑦⟶𝐽) → 𝐽 ∈ V) |
32 | | simpr 477 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅}))
∧ 𝑓:𝑦⟶𝐽) → 𝑓:𝑦⟶𝐽) |
33 | 8 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅}))
∧ 𝑓:𝑦⟶𝐽) → 𝑦 ∈ Fin) |
34 | | intrnfi 8322 |
. . . . . . . . . . . . . . 15
⊢ ((𝐽 ∈ V ∧ (𝑓:𝑦⟶𝐽 ∧ 𝑦 ≠ ∅ ∧ 𝑦 ∈ Fin)) → ∩ ran 𝑓 ∈ (fi‘𝐽)) |
35 | 31, 32, 21, 33, 34 | syl13anc 1328 |
. . . . . . . . . . . . . 14
⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅}))
∧ 𝑓:𝑦⟶𝐽) → ∩ ran
𝑓 ∈ (fi‘𝐽)) |
36 | 30, 35 | eqeltrd 2701 |
. . . . . . . . . . . . 13
⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅}))
∧ 𝑓:𝑦⟶𝐽) → ∩
𝑧 ∈ 𝑦 (𝑓‘𝑧) ∈ (fi‘𝐽)) |
37 | | elrestr 16089 |
. . . . . . . . . . . . 13
⊢
(((fi‘𝐽)
∈ V ∧ 𝐴 ∈ V
∧ ∩ 𝑧 ∈ 𝑦 (𝑓‘𝑧) ∈ (fi‘𝐽)) → (∩ 𝑧 ∈ 𝑦 (𝑓‘𝑧) ∩ 𝐴) ∈ ((fi‘𝐽) ↾t 𝐴)) |
38 | 25, 26, 36, 37 | syl3anc 1326 |
. . . . . . . . . . . 12
⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅}))
∧ 𝑓:𝑦⟶𝐽) → (∩ 𝑧 ∈ 𝑦 (𝑓‘𝑧) ∩ 𝐴) ∈ ((fi‘𝐽) ↾t 𝐴)) |
39 | 23, 38 | eqeltrd 2701 |
. . . . . . . . . . 11
⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅}))
∧ 𝑓:𝑦⟶𝐽) → ∩
𝑧 ∈ 𝑦 ((𝑓‘𝑧) ∩ 𝐴) ∈ ((fi‘𝐽) ↾t 𝐴)) |
40 | | intiin 4574 |
. . . . . . . . . . . . 13
⊢ ∩ 𝑦 =
∩ 𝑧 ∈ 𝑦 𝑧 |
41 | | iineq2 4538 |
. . . . . . . . . . . . 13
⊢
(∀𝑧 ∈
𝑦 𝑧 = ((𝑓‘𝑧) ∩ 𝐴) → ∩
𝑧 ∈ 𝑦 𝑧 = ∩ 𝑧 ∈ 𝑦 ((𝑓‘𝑧) ∩ 𝐴)) |
42 | 40, 41 | syl5eq 2668 |
. . . . . . . . . . . 12
⊢
(∀𝑧 ∈
𝑦 𝑧 = ((𝑓‘𝑧) ∩ 𝐴) → ∩ 𝑦 = ∩ 𝑧 ∈ 𝑦 ((𝑓‘𝑧) ∩ 𝐴)) |
43 | 42 | eleq1d 2686 |
. . . . . . . . . . 11
⊢
(∀𝑧 ∈
𝑦 𝑧 = ((𝑓‘𝑧) ∩ 𝐴) → (∩ 𝑦 ∈ ((fi‘𝐽) ↾t 𝐴) ↔ ∩ 𝑧 ∈ 𝑦 ((𝑓‘𝑧) ∩ 𝐴) ∈ ((fi‘𝐽) ↾t 𝐴))) |
44 | 39, 43 | syl5ibrcom 237 |
. . . . . . . . . 10
⊢ ((((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅}))
∧ 𝑓:𝑦⟶𝐽) → (∀𝑧 ∈ 𝑦 𝑧 = ((𝑓‘𝑧) ∩ 𝐴) → ∩ 𝑦 ∈ ((fi‘𝐽) ↾t 𝐴))) |
45 | 44 | expimpd 629 |
. . . . . . . . 9
⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅}))
→ ((𝑓:𝑦⟶𝐽 ∧ ∀𝑧 ∈ 𝑦 𝑧 = ((𝑓‘𝑧) ∩ 𝐴)) → ∩ 𝑦 ∈ ((fi‘𝐽) ↾t 𝐴))) |
46 | 45 | exlimdv 1861 |
. . . . . . . 8
⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅}))
→ (∃𝑓(𝑓:𝑦⟶𝐽 ∧ ∀𝑧 ∈ 𝑦 𝑧 = ((𝑓‘𝑧) ∩ 𝐴)) → ∩ 𝑦 ∈ ((fi‘𝐽) ↾t 𝐴))) |
47 | 19, 46 | mpd 15 |
. . . . . . 7
⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅}))
→ ∩ 𝑦 ∈ ((fi‘𝐽) ↾t 𝐴)) |
48 | | eleq1 2689 |
. . . . . . 7
⊢ (𝑥 = ∩
𝑦 → (𝑥 ∈ ((fi‘𝐽) ↾t 𝐴) ↔ ∩ 𝑦
∈ ((fi‘𝐽)
↾t 𝐴))) |
49 | 47, 48 | syl5ibrcom 237 |
. . . . . 6
⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖ {∅}))
→ (𝑥 = ∩ 𝑦
→ 𝑥 ∈
((fi‘𝐽)
↾t 𝐴))) |
50 | 49 | rexlimdva 3031 |
. . . . 5
⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V) → (∃𝑦 ∈ ((𝒫 (𝐽 ↾t 𝐴) ∩ Fin) ∖
{∅})𝑥 = ∩ 𝑦
→ 𝑥 ∈
((fi‘𝐽)
↾t 𝐴))) |
51 | 3, 50 | syl5bi 232 |
. . . 4
⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V) → (𝑥 ∈ (fi‘(𝐽 ↾t 𝐴)) → 𝑥 ∈ ((fi‘𝐽) ↾t 𝐴))) |
52 | | simpr 477 |
. . . . . 6
⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V) → 𝐴 ∈ V) |
53 | | elrest 16088 |
. . . . . 6
⊢
(((fi‘𝐽)
∈ V ∧ 𝐴 ∈ V)
→ (𝑥 ∈
((fi‘𝐽)
↾t 𝐴)
↔ ∃𝑧 ∈
(fi‘𝐽)𝑥 = (𝑧 ∩ 𝐴))) |
54 | 24, 52, 53 | sylancr 695 |
. . . . 5
⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V) → (𝑥 ∈ ((fi‘𝐽) ↾t 𝐴) ↔ ∃𝑧 ∈ (fi‘𝐽)𝑥 = (𝑧 ∩ 𝐴))) |
55 | | elfi2 8320 |
. . . . . . . 8
⊢ (𝐽 ∈ V → (𝑧 ∈ (fi‘𝐽) ↔ ∃𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖
{∅})𝑧 = ∩ 𝑦)) |
56 | 55 | adantr 481 |
. . . . . . 7
⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V) → (𝑧 ∈ (fi‘𝐽) ↔ ∃𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖
{∅})𝑧 = ∩ 𝑦)) |
57 | | eldifsni 4320 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅})
→ 𝑦 ≠
∅) |
58 | 57 | adantl 482 |
. . . . . . . . . . . . 13
⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅}))
→ 𝑦 ≠
∅) |
59 | | iinin1 4591 |
. . . . . . . . . . . . 13
⊢ (𝑦 ≠ ∅ → ∩ 𝑧 ∈ 𝑦 (𝑧 ∩ 𝐴) = (∩
𝑧 ∈ 𝑦 𝑧 ∩ 𝐴)) |
60 | 58, 59 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅}))
→ ∩ 𝑧 ∈ 𝑦 (𝑧 ∩ 𝐴) = (∩
𝑧 ∈ 𝑦 𝑧 ∩ 𝐴)) |
61 | 40 | ineq1i 3810 |
. . . . . . . . . . . 12
⊢ (∩ 𝑦
∩ 𝐴) = (∩ 𝑧 ∈ 𝑦 𝑧 ∩ 𝐴) |
62 | 60, 61 | syl6eqr 2674 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅}))
→ ∩ 𝑧 ∈ 𝑦 (𝑧 ∩ 𝐴) = (∩ 𝑦 ∩ 𝐴)) |
63 | 1 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅}))
→ (𝐽
↾t 𝐴)
∈ V) |
64 | | eldifi 3732 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅})
→ 𝑦 ∈ (𝒫
𝐽 ∩
Fin)) |
65 | 64 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅}))
→ 𝑦 ∈ (𝒫
𝐽 ∩
Fin)) |
66 | | elfpw 8268 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ (𝒫 𝐽 ∩ Fin) ↔ (𝑦 ⊆ 𝐽 ∧ 𝑦 ∈ Fin)) |
67 | 66 | simplbi 476 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ (𝒫 𝐽 ∩ Fin) → 𝑦 ⊆ 𝐽) |
68 | 65, 67 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅}))
→ 𝑦 ⊆ 𝐽) |
69 | | elrestr 16089 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V ∧ 𝑧 ∈ 𝐽) → (𝑧 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴)) |
70 | 69 | 3expa 1265 |
. . . . . . . . . . . . . . 15
⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑧 ∈ 𝐽) → (𝑧 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴)) |
71 | 70 | ralrimiva 2966 |
. . . . . . . . . . . . . 14
⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V) → ∀𝑧 ∈ 𝐽 (𝑧 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴)) |
72 | 71 | adantr 481 |
. . . . . . . . . . . . 13
⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅}))
→ ∀𝑧 ∈
𝐽 (𝑧 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴)) |
73 | | ssralv 3666 |
. . . . . . . . . . . . 13
⊢ (𝑦 ⊆ 𝐽 → (∀𝑧 ∈ 𝐽 (𝑧 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴) → ∀𝑧 ∈ 𝑦 (𝑧 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴))) |
74 | 68, 72, 73 | sylc 65 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅}))
→ ∀𝑧 ∈
𝑦 (𝑧 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴)) |
75 | 66 | simprbi 480 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ (𝒫 𝐽 ∩ Fin) → 𝑦 ∈ Fin) |
76 | 65, 75 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅}))
→ 𝑦 ∈
Fin) |
77 | | iinfi 8323 |
. . . . . . . . . . . 12
⊢ (((𝐽 ↾t 𝐴) ∈ V ∧ (∀𝑧 ∈ 𝑦 (𝑧 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴) ∧ 𝑦 ≠ ∅ ∧ 𝑦 ∈ Fin)) → ∩ 𝑧 ∈ 𝑦 (𝑧 ∩ 𝐴) ∈ (fi‘(𝐽 ↾t 𝐴))) |
78 | 63, 74, 58, 76, 77 | syl13anc 1328 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅}))
→ ∩ 𝑧 ∈ 𝑦 (𝑧 ∩ 𝐴) ∈ (fi‘(𝐽 ↾t 𝐴))) |
79 | 62, 78 | eqeltrrd 2702 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅}))
→ (∩ 𝑦 ∩ 𝐴) ∈ (fi‘(𝐽 ↾t 𝐴))) |
80 | | eleq1 2689 |
. . . . . . . . . 10
⊢ (𝑥 = (∩
𝑦 ∩ 𝐴) → (𝑥 ∈ (fi‘(𝐽 ↾t 𝐴)) ↔ (∩
𝑦 ∩ 𝐴) ∈ (fi‘(𝐽 ↾t 𝐴)))) |
81 | 79, 80 | syl5ibrcom 237 |
. . . . . . . . 9
⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅}))
→ (𝑥 = (∩ 𝑦
∩ 𝐴) → 𝑥 ∈ (fi‘(𝐽 ↾t 𝐴)))) |
82 | | ineq1 3807 |
. . . . . . . . . . 11
⊢ (𝑧 = ∩
𝑦 → (𝑧 ∩ 𝐴) = (∩ 𝑦 ∩ 𝐴)) |
83 | 82 | eqeq2d 2632 |
. . . . . . . . . 10
⊢ (𝑧 = ∩
𝑦 → (𝑥 = (𝑧 ∩ 𝐴) ↔ 𝑥 = (∩ 𝑦 ∩ 𝐴))) |
84 | 83 | imbi1d 331 |
. . . . . . . . 9
⊢ (𝑧 = ∩
𝑦 → ((𝑥 = (𝑧 ∩ 𝐴) → 𝑥 ∈ (fi‘(𝐽 ↾t 𝐴))) ↔ (𝑥 = (∩ 𝑦 ∩ 𝐴) → 𝑥 ∈ (fi‘(𝐽 ↾t 𝐴))))) |
85 | 81, 84 | syl5ibrcom 237 |
. . . . . . . 8
⊢ (((𝐽 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖ {∅}))
→ (𝑧 = ∩ 𝑦
→ (𝑥 = (𝑧 ∩ 𝐴) → 𝑥 ∈ (fi‘(𝐽 ↾t 𝐴))))) |
86 | 85 | rexlimdva 3031 |
. . . . . . 7
⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V) → (∃𝑦 ∈ ((𝒫 𝐽 ∩ Fin) ∖
{∅})𝑧 = ∩ 𝑦
→ (𝑥 = (𝑧 ∩ 𝐴) → 𝑥 ∈ (fi‘(𝐽 ↾t 𝐴))))) |
87 | 56, 86 | sylbid 230 |
. . . . . 6
⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V) → (𝑧 ∈ (fi‘𝐽) → (𝑥 = (𝑧 ∩ 𝐴) → 𝑥 ∈ (fi‘(𝐽 ↾t 𝐴))))) |
88 | 87 | rexlimdv 3030 |
. . . . 5
⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V) → (∃𝑧 ∈ (fi‘𝐽)𝑥 = (𝑧 ∩ 𝐴) → 𝑥 ∈ (fi‘(𝐽 ↾t 𝐴)))) |
89 | 54, 88 | sylbid 230 |
. . . 4
⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V) → (𝑥 ∈ ((fi‘𝐽) ↾t 𝐴) → 𝑥 ∈ (fi‘(𝐽 ↾t 𝐴)))) |
90 | 51, 89 | impbid 202 |
. . 3
⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V) → (𝑥 ∈ (fi‘(𝐽 ↾t 𝐴)) ↔ 𝑥 ∈ ((fi‘𝐽) ↾t 𝐴))) |
91 | 90 | eqrdv 2620 |
. 2
⊢ ((𝐽 ∈ V ∧ 𝐴 ∈ V) →
(fi‘(𝐽
↾t 𝐴)) =
((fi‘𝐽)
↾t 𝐴)) |
92 | | fi0 8326 |
. . 3
⊢
(fi‘∅) = ∅ |
93 | | relxp 5227 |
. . . . . 6
⊢ Rel (V
× V) |
94 | | restfn 16085 |
. . . . . . . 8
⊢
↾t Fn (V × V) |
95 | | fndm 5990 |
. . . . . . . 8
⊢ (
↾t Fn (V × V) → dom ↾t = (V
× V)) |
96 | 94, 95 | ax-mp 5 |
. . . . . . 7
⊢ dom
↾t = (V × V) |
97 | 96 | releqi 5202 |
. . . . . 6
⊢ (Rel dom
↾t ↔ Rel (V × V)) |
98 | 93, 97 | mpbir 221 |
. . . . 5
⊢ Rel dom
↾t |
99 | 98 | ovprc 6683 |
. . . 4
⊢ (¬
(𝐽 ∈ V ∧ 𝐴 ∈ V) → (𝐽 ↾t 𝐴) = ∅) |
100 | 99 | fveq2d 6195 |
. . 3
⊢ (¬
(𝐽 ∈ V ∧ 𝐴 ∈ V) →
(fi‘(𝐽
↾t 𝐴)) =
(fi‘∅)) |
101 | | ianor 509 |
. . . 4
⊢ (¬
(𝐽 ∈ V ∧ 𝐴 ∈ V) ↔ (¬ 𝐽 ∈ V ∨ ¬ 𝐴 ∈ V)) |
102 | | fvprc 6185 |
. . . . . . 7
⊢ (¬
𝐽 ∈ V →
(fi‘𝐽) =
∅) |
103 | 102 | oveq1d 6665 |
. . . . . 6
⊢ (¬
𝐽 ∈ V →
((fi‘𝐽)
↾t 𝐴) =
(∅ ↾t 𝐴)) |
104 | | 0rest 16090 |
. . . . . 6
⊢ (∅
↾t 𝐴) =
∅ |
105 | 103, 104 | syl6eq 2672 |
. . . . 5
⊢ (¬
𝐽 ∈ V →
((fi‘𝐽)
↾t 𝐴) =
∅) |
106 | 98 | ovprc2 6685 |
. . . . 5
⊢ (¬
𝐴 ∈ V →
((fi‘𝐽)
↾t 𝐴) =
∅) |
107 | 105, 106 | jaoi 394 |
. . . 4
⊢ ((¬
𝐽 ∈ V ∨ ¬ 𝐴 ∈ V) →
((fi‘𝐽)
↾t 𝐴) =
∅) |
108 | 101, 107 | sylbi 207 |
. . 3
⊢ (¬
(𝐽 ∈ V ∧ 𝐴 ∈ V) →
((fi‘𝐽)
↾t 𝐴) =
∅) |
109 | 92, 100, 108 | 3eqtr4a 2682 |
. 2
⊢ (¬
(𝐽 ∈ V ∧ 𝐴 ∈ V) →
(fi‘(𝐽
↾t 𝐴)) =
((fi‘𝐽)
↾t 𝐴)) |
110 | 91, 109 | pm2.61i 176 |
1
⊢
(fi‘(𝐽
↾t 𝐴)) =
((fi‘𝐽)
↾t 𝐴) |