Step | Hyp | Ref
| Expression |
1 | | ovex 6678 |
. 2
⊢
(𝒫 ∪ ran 𝐽 ↑pm dom 𝐽) ∈ V |
2 | | brssc 16474 |
. . . 4
⊢ (ℎ ⊆cat 𝐽 ↔ ∃𝑡(𝐽 Fn (𝑡 × 𝑡) ∧ ∃𝑠 ∈ 𝒫 𝑡ℎ ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑥))) |
3 | | simpl 473 |
. . . . . . . . . 10
⊢ ((𝐽 Fn (𝑡 × 𝑡) ∧ (𝑠 ∈ 𝒫 𝑡 ∧ ℎ ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑥))) → 𝐽 Fn (𝑡 × 𝑡)) |
4 | | vex 3203 |
. . . . . . . . . . 11
⊢ 𝑡 ∈ V |
5 | 4, 4 | xpex 6962 |
. . . . . . . . . 10
⊢ (𝑡 × 𝑡) ∈ V |
6 | | fnex 6481 |
. . . . . . . . . 10
⊢ ((𝐽 Fn (𝑡 × 𝑡) ∧ (𝑡 × 𝑡) ∈ V) → 𝐽 ∈ V) |
7 | 3, 5, 6 | sylancl 694 |
. . . . . . . . 9
⊢ ((𝐽 Fn (𝑡 × 𝑡) ∧ (𝑠 ∈ 𝒫 𝑡 ∧ ℎ ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑥))) → 𝐽 ∈ V) |
8 | | rnexg 7098 |
. . . . . . . . 9
⊢ (𝐽 ∈ V → ran 𝐽 ∈ V) |
9 | | uniexg 6955 |
. . . . . . . . 9
⊢ (ran
𝐽 ∈ V → ∪ ran 𝐽 ∈ V) |
10 | | pwexg 4850 |
. . . . . . . . 9
⊢ (∪ ran 𝐽 ∈ V → 𝒫 ∪ ran 𝐽 ∈ V) |
11 | 7, 8, 9, 10 | 4syl 19 |
. . . . . . . 8
⊢ ((𝐽 Fn (𝑡 × 𝑡) ∧ (𝑠 ∈ 𝒫 𝑡 ∧ ℎ ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑥))) → 𝒫 ∪ ran 𝐽 ∈ V) |
12 | | fndm 5990 |
. . . . . . . . . 10
⊢ (𝐽 Fn (𝑡 × 𝑡) → dom 𝐽 = (𝑡 × 𝑡)) |
13 | 12 | adantr 481 |
. . . . . . . . 9
⊢ ((𝐽 Fn (𝑡 × 𝑡) ∧ (𝑠 ∈ 𝒫 𝑡 ∧ ℎ ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑥))) → dom 𝐽 = (𝑡 × 𝑡)) |
14 | 13, 5 | syl6eqel 2709 |
. . . . . . . 8
⊢ ((𝐽 Fn (𝑡 × 𝑡) ∧ (𝑠 ∈ 𝒫 𝑡 ∧ ℎ ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑥))) → dom 𝐽 ∈ V) |
15 | | ss2ixp 7921 |
. . . . . . . . . . 11
⊢
(∀𝑥 ∈
(𝑠 × 𝑠)𝒫 (𝐽‘𝑥) ⊆ 𝒫 ∪ ran 𝐽 → X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑥) ⊆ X𝑥 ∈ (𝑠 × 𝑠)𝒫 ∪ ran
𝐽) |
16 | | fvssunirn 6217 |
. . . . . . . . . . . . 13
⊢ (𝐽‘𝑥) ⊆ ∪ ran
𝐽 |
17 | | sspwb 4917 |
. . . . . . . . . . . . 13
⊢ ((𝐽‘𝑥) ⊆ ∪ ran
𝐽 ↔ 𝒫 (𝐽‘𝑥) ⊆ 𝒫 ∪ ran 𝐽) |
18 | 16, 17 | mpbi 220 |
. . . . . . . . . . . 12
⊢ 𝒫
(𝐽‘𝑥) ⊆ 𝒫 ∪ ran 𝐽 |
19 | 18 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (𝑠 × 𝑠) → 𝒫 (𝐽‘𝑥) ⊆ 𝒫 ∪ ran 𝐽) |
20 | 15, 19 | mprg 2926 |
. . . . . . . . . 10
⊢ X𝑥 ∈
(𝑠 × 𝑠)𝒫 (𝐽‘𝑥) ⊆ X𝑥 ∈ (𝑠 × 𝑠)𝒫 ∪ ran
𝐽 |
21 | | simprr 796 |
. . . . . . . . . 10
⊢ ((𝐽 Fn (𝑡 × 𝑡) ∧ (𝑠 ∈ 𝒫 𝑡 ∧ ℎ ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑥))) → ℎ ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑥)) |
22 | 20, 21 | sseldi 3601 |
. . . . . . . . 9
⊢ ((𝐽 Fn (𝑡 × 𝑡) ∧ (𝑠 ∈ 𝒫 𝑡 ∧ ℎ ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑥))) → ℎ ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 ∪ ran
𝐽) |
23 | | vex 3203 |
. . . . . . . . . 10
⊢ ℎ ∈ V |
24 | 23 | elixpconst 7916 |
. . . . . . . . 9
⊢ (ℎ ∈ X𝑥 ∈
(𝑠 × 𝑠)𝒫 ∪ ran 𝐽 ↔ ℎ:(𝑠 × 𝑠)⟶𝒫 ∪ ran 𝐽) |
25 | 22, 24 | sylib 208 |
. . . . . . . 8
⊢ ((𝐽 Fn (𝑡 × 𝑡) ∧ (𝑠 ∈ 𝒫 𝑡 ∧ ℎ ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑥))) → ℎ:(𝑠 × 𝑠)⟶𝒫 ∪ ran 𝐽) |
26 | | elpwi 4168 |
. . . . . . . . . . 11
⊢ (𝑠 ∈ 𝒫 𝑡 → 𝑠 ⊆ 𝑡) |
27 | 26 | ad2antrl 764 |
. . . . . . . . . 10
⊢ ((𝐽 Fn (𝑡 × 𝑡) ∧ (𝑠 ∈ 𝒫 𝑡 ∧ ℎ ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑥))) → 𝑠 ⊆ 𝑡) |
28 | | xpss12 5225 |
. . . . . . . . . 10
⊢ ((𝑠 ⊆ 𝑡 ∧ 𝑠 ⊆ 𝑡) → (𝑠 × 𝑠) ⊆ (𝑡 × 𝑡)) |
29 | 27, 27, 28 | syl2anc 693 |
. . . . . . . . 9
⊢ ((𝐽 Fn (𝑡 × 𝑡) ∧ (𝑠 ∈ 𝒫 𝑡 ∧ ℎ ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑥))) → (𝑠 × 𝑠) ⊆ (𝑡 × 𝑡)) |
30 | 29, 13 | sseqtr4d 3642 |
. . . . . . . 8
⊢ ((𝐽 Fn (𝑡 × 𝑡) ∧ (𝑠 ∈ 𝒫 𝑡 ∧ ℎ ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑥))) → (𝑠 × 𝑠) ⊆ dom 𝐽) |
31 | | elpm2r 7875 |
. . . . . . . 8
⊢
(((𝒫 ∪ ran 𝐽 ∈ V ∧ dom 𝐽 ∈ V) ∧ (ℎ:(𝑠 × 𝑠)⟶𝒫 ∪ ran 𝐽 ∧ (𝑠 × 𝑠) ⊆ dom 𝐽)) → ℎ ∈ (𝒫 ∪ ran 𝐽 ↑pm dom 𝐽)) |
32 | 11, 14, 25, 30, 31 | syl22anc 1327 |
. . . . . . 7
⊢ ((𝐽 Fn (𝑡 × 𝑡) ∧ (𝑠 ∈ 𝒫 𝑡 ∧ ℎ ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑥))) → ℎ ∈ (𝒫 ∪ ran 𝐽 ↑pm dom 𝐽)) |
33 | 32 | rexlimdvaa 3032 |
. . . . . 6
⊢ (𝐽 Fn (𝑡 × 𝑡) → (∃𝑠 ∈ 𝒫 𝑡ℎ ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑥) → ℎ ∈ (𝒫 ∪ ran 𝐽 ↑pm dom 𝐽))) |
34 | 33 | imp 445 |
. . . . 5
⊢ ((𝐽 Fn (𝑡 × 𝑡) ∧ ∃𝑠 ∈ 𝒫 𝑡ℎ ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑥)) → ℎ ∈ (𝒫 ∪ ran 𝐽 ↑pm dom 𝐽)) |
35 | 34 | exlimiv 1858 |
. . . 4
⊢
(∃𝑡(𝐽 Fn (𝑡 × 𝑡) ∧ ∃𝑠 ∈ 𝒫 𝑡ℎ ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑥)) → ℎ ∈ (𝒫 ∪ ran 𝐽 ↑pm dom 𝐽)) |
36 | 2, 35 | sylbi 207 |
. . 3
⊢ (ℎ ⊆cat 𝐽 → ℎ ∈ (𝒫 ∪ ran 𝐽 ↑pm dom 𝐽)) |
37 | 36 | abssi 3677 |
. 2
⊢ {ℎ ∣ ℎ ⊆cat 𝐽} ⊆ (𝒫 ∪ ran 𝐽 ↑pm dom 𝐽) |
38 | 1, 37 | ssexi 4803 |
1
⊢ {ℎ ∣ ℎ ⊆cat 𝐽} ∈ V |