Step | Hyp | Ref
| Expression |
1 | | brssc 17078 |
. . . 4
⊢ (𝐻 ⊆cat 𝐽 ↔ ∃𝑡(𝐽 Fn (𝑡 × 𝑡) ∧ ∃𝑠 ∈ 𝒫 𝑡𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧))) |
2 | | fndm 6449 |
. . . . . . . . . . . 12
⊢ (𝐽 Fn (𝑡 × 𝑡) → dom 𝐽 = (𝑡 × 𝑡)) |
3 | 2 | adantl 484 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐽 Fn (𝑡 × 𝑡)) → dom 𝐽 = (𝑡 × 𝑡)) |
4 | | isssc.2 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐽 Fn (𝑇 × 𝑇)) |
5 | 4 | adantr 483 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐽 Fn (𝑡 × 𝑡)) → 𝐽 Fn (𝑇 × 𝑇)) |
6 | | fndm 6449 |
. . . . . . . . . . . 12
⊢ (𝐽 Fn (𝑇 × 𝑇) → dom 𝐽 = (𝑇 × 𝑇)) |
7 | 5, 6 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐽 Fn (𝑡 × 𝑡)) → dom 𝐽 = (𝑇 × 𝑇)) |
8 | 3, 7 | eqtr3d 2858 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐽 Fn (𝑡 × 𝑡)) → (𝑡 × 𝑡) = (𝑇 × 𝑇)) |
9 | 8 | dmeqd 5768 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐽 Fn (𝑡 × 𝑡)) → dom (𝑡 × 𝑡) = dom (𝑇 × 𝑇)) |
10 | | dmxpid 5794 |
. . . . . . . . 9
⊢ dom
(𝑡 × 𝑡) = 𝑡 |
11 | | dmxpid 5794 |
. . . . . . . . 9
⊢ dom
(𝑇 × 𝑇) = 𝑇 |
12 | 9, 10, 11 | 3eqtr3g 2879 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐽 Fn (𝑡 × 𝑡)) → 𝑡 = 𝑇) |
13 | 12 | ex 415 |
. . . . . . 7
⊢ (𝜑 → (𝐽 Fn (𝑡 × 𝑡) → 𝑡 = 𝑇)) |
14 | | id 22 |
. . . . . . . . . 10
⊢ (𝑡 = 𝑇 → 𝑡 = 𝑇) |
15 | 14 | sqxpeqd 5581 |
. . . . . . . . 9
⊢ (𝑡 = 𝑇 → (𝑡 × 𝑡) = (𝑇 × 𝑇)) |
16 | 15 | fneq2d 6441 |
. . . . . . . 8
⊢ (𝑡 = 𝑇 → (𝐽 Fn (𝑡 × 𝑡) ↔ 𝐽 Fn (𝑇 × 𝑇))) |
17 | 4, 16 | syl5ibrcom 249 |
. . . . . . 7
⊢ (𝜑 → (𝑡 = 𝑇 → 𝐽 Fn (𝑡 × 𝑡))) |
18 | 13, 17 | impbid 214 |
. . . . . 6
⊢ (𝜑 → (𝐽 Fn (𝑡 × 𝑡) ↔ 𝑡 = 𝑇)) |
19 | 18 | anbi1d 631 |
. . . . 5
⊢ (𝜑 → ((𝐽 Fn (𝑡 × 𝑡) ∧ ∃𝑠 ∈ 𝒫 𝑡𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧)) ↔ (𝑡 = 𝑇 ∧ ∃𝑠 ∈ 𝒫 𝑡𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧)))) |
20 | 19 | exbidv 1918 |
. . . 4
⊢ (𝜑 → (∃𝑡(𝐽 Fn (𝑡 × 𝑡) ∧ ∃𝑠 ∈ 𝒫 𝑡𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧)) ↔ ∃𝑡(𝑡 = 𝑇 ∧ ∃𝑠 ∈ 𝒫 𝑡𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧)))) |
21 | 1, 20 | syl5bb 285 |
. . 3
⊢ (𝜑 → (𝐻 ⊆cat 𝐽 ↔ ∃𝑡(𝑡 = 𝑇 ∧ ∃𝑠 ∈ 𝒫 𝑡𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧)))) |
22 | | isssc.3 |
. . . 4
⊢ (𝜑 → 𝑇 ∈ 𝑉) |
23 | | pweq 4541 |
. . . . . 6
⊢ (𝑡 = 𝑇 → 𝒫 𝑡 = 𝒫 𝑇) |
24 | 23 | rexeqdv 3416 |
. . . . 5
⊢ (𝑡 = 𝑇 → (∃𝑠 ∈ 𝒫 𝑡𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧) ↔ ∃𝑠 ∈ 𝒫 𝑇𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧))) |
25 | 24 | ceqsexgv 3646 |
. . . 4
⊢ (𝑇 ∈ 𝑉 → (∃𝑡(𝑡 = 𝑇 ∧ ∃𝑠 ∈ 𝒫 𝑡𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧)) ↔ ∃𝑠 ∈ 𝒫 𝑇𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧))) |
26 | 22, 25 | syl 17 |
. . 3
⊢ (𝜑 → (∃𝑡(𝑡 = 𝑇 ∧ ∃𝑠 ∈ 𝒫 𝑡𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧)) ↔ ∃𝑠 ∈ 𝒫 𝑇𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧))) |
27 | 21, 26 | bitrd 281 |
. 2
⊢ (𝜑 → (𝐻 ⊆cat 𝐽 ↔ ∃𝑠 ∈ 𝒫 𝑇𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧))) |
28 | | df-rex 3144 |
. . 3
⊢
(∃𝑠 ∈
𝒫 𝑇𝐻 ∈ X𝑧 ∈
(𝑠 × 𝑠)𝒫 (𝐽‘𝑧) ↔ ∃𝑠(𝑠 ∈ 𝒫 𝑇 ∧ 𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧))) |
29 | | 3anass 1091 |
. . . . . . . 8
⊢ ((𝐻 ∈ V ∧ 𝐻 Fn (𝑠 × 𝑠) ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧)) ↔ (𝐻 ∈ V ∧ (𝐻 Fn (𝑠 × 𝑠) ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧)))) |
30 | | elixp2 8459 |
. . . . . . . 8
⊢ (𝐻 ∈ X𝑧 ∈
(𝑠 × 𝑠)𝒫 (𝐽‘𝑧) ↔ (𝐻 ∈ V ∧ 𝐻 Fn (𝑠 × 𝑠) ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧))) |
31 | | vex 3497 |
. . . . . . . . . . . 12
⊢ 𝑠 ∈ V |
32 | 31, 31 | xpex 7470 |
. . . . . . . . . . 11
⊢ (𝑠 × 𝑠) ∈ V |
33 | | fnex 6974 |
. . . . . . . . . . 11
⊢ ((𝐻 Fn (𝑠 × 𝑠) ∧ (𝑠 × 𝑠) ∈ V) → 𝐻 ∈ V) |
34 | 32, 33 | mpan2 689 |
. . . . . . . . . 10
⊢ (𝐻 Fn (𝑠 × 𝑠) → 𝐻 ∈ V) |
35 | 34 | adantr 483 |
. . . . . . . . 9
⊢ ((𝐻 Fn (𝑠 × 𝑠) ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧)) → 𝐻 ∈ V) |
36 | 35 | pm4.71ri 563 |
. . . . . . . 8
⊢ ((𝐻 Fn (𝑠 × 𝑠) ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧)) ↔ (𝐻 ∈ V ∧ (𝐻 Fn (𝑠 × 𝑠) ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧)))) |
37 | 29, 30, 36 | 3bitr4i 305 |
. . . . . . 7
⊢ (𝐻 ∈ X𝑧 ∈
(𝑠 × 𝑠)𝒫 (𝐽‘𝑧) ↔ (𝐻 Fn (𝑠 × 𝑠) ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧))) |
38 | | fndm 6449 |
. . . . . . . . . . . . . 14
⊢ (𝐻 Fn (𝑠 × 𝑠) → dom 𝐻 = (𝑠 × 𝑠)) |
39 | 38 | adantl 484 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐻 Fn (𝑠 × 𝑠)) → dom 𝐻 = (𝑠 × 𝑠)) |
40 | | isssc.1 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆)) |
41 | 40 | adantr 483 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝐻 Fn (𝑠 × 𝑠)) → 𝐻 Fn (𝑆 × 𝑆)) |
42 | | fndm 6449 |
. . . . . . . . . . . . . 14
⊢ (𝐻 Fn (𝑆 × 𝑆) → dom 𝐻 = (𝑆 × 𝑆)) |
43 | 41, 42 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐻 Fn (𝑠 × 𝑠)) → dom 𝐻 = (𝑆 × 𝑆)) |
44 | 39, 43 | eqtr3d 2858 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐻 Fn (𝑠 × 𝑠)) → (𝑠 × 𝑠) = (𝑆 × 𝑆)) |
45 | 44 | dmeqd 5768 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐻 Fn (𝑠 × 𝑠)) → dom (𝑠 × 𝑠) = dom (𝑆 × 𝑆)) |
46 | | dmxpid 5794 |
. . . . . . . . . . 11
⊢ dom
(𝑠 × 𝑠) = 𝑠 |
47 | | dmxpid 5794 |
. . . . . . . . . . 11
⊢ dom
(𝑆 × 𝑆) = 𝑆 |
48 | 45, 46, 47 | 3eqtr3g 2879 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐻 Fn (𝑠 × 𝑠)) → 𝑠 = 𝑆) |
49 | 48 | ex 415 |
. . . . . . . . 9
⊢ (𝜑 → (𝐻 Fn (𝑠 × 𝑠) → 𝑠 = 𝑆)) |
50 | | id 22 |
. . . . . . . . . . . 12
⊢ (𝑠 = 𝑆 → 𝑠 = 𝑆) |
51 | 50 | sqxpeqd 5581 |
. . . . . . . . . . 11
⊢ (𝑠 = 𝑆 → (𝑠 × 𝑠) = (𝑆 × 𝑆)) |
52 | 51 | fneq2d 6441 |
. . . . . . . . . 10
⊢ (𝑠 = 𝑆 → (𝐻 Fn (𝑠 × 𝑠) ↔ 𝐻 Fn (𝑆 × 𝑆))) |
53 | 40, 52 | syl5ibrcom 249 |
. . . . . . . . 9
⊢ (𝜑 → (𝑠 = 𝑆 → 𝐻 Fn (𝑠 × 𝑠))) |
54 | 49, 53 | impbid 214 |
. . . . . . . 8
⊢ (𝜑 → (𝐻 Fn (𝑠 × 𝑠) ↔ 𝑠 = 𝑆)) |
55 | 54 | anbi1d 631 |
. . . . . . 7
⊢ (𝜑 → ((𝐻 Fn (𝑠 × 𝑠) ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧)) ↔ (𝑠 = 𝑆 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧)))) |
56 | 37, 55 | syl5bb 285 |
. . . . . 6
⊢ (𝜑 → (𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧) ↔ (𝑠 = 𝑆 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧)))) |
57 | 56 | anbi2d 630 |
. . . . 5
⊢ (𝜑 → ((𝑠 ∈ 𝒫 𝑇 ∧ 𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧)) ↔ (𝑠 ∈ 𝒫 𝑇 ∧ (𝑠 = 𝑆 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧))))) |
58 | | an12 643 |
. . . . 5
⊢ ((𝑠 ∈ 𝒫 𝑇 ∧ (𝑠 = 𝑆 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧))) ↔ (𝑠 = 𝑆 ∧ (𝑠 ∈ 𝒫 𝑇 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧)))) |
59 | 57, 58 | syl6bb 289 |
. . . 4
⊢ (𝜑 → ((𝑠 ∈ 𝒫 𝑇 ∧ 𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧)) ↔ (𝑠 = 𝑆 ∧ (𝑠 ∈ 𝒫 𝑇 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧))))) |
60 | 59 | exbidv 1918 |
. . 3
⊢ (𝜑 → (∃𝑠(𝑠 ∈ 𝒫 𝑇 ∧ 𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧)) ↔ ∃𝑠(𝑠 = 𝑆 ∧ (𝑠 ∈ 𝒫 𝑇 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧))))) |
61 | 28, 60 | syl5bb 285 |
. 2
⊢ (𝜑 → (∃𝑠 ∈ 𝒫 𝑇𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧) ↔ ∃𝑠(𝑠 = 𝑆 ∧ (𝑠 ∈ 𝒫 𝑇 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧))))) |
62 | | exsimpl 1865 |
. . . . 5
⊢
(∃𝑠(𝑠 = 𝑆 ∧ (𝑠 ∈ 𝒫 𝑇 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧))) → ∃𝑠 𝑠 = 𝑆) |
63 | | isset 3506 |
. . . . 5
⊢ (𝑆 ∈ V ↔ ∃𝑠 𝑠 = 𝑆) |
64 | 62, 63 | sylibr 236 |
. . . 4
⊢
(∃𝑠(𝑠 = 𝑆 ∧ (𝑠 ∈ 𝒫 𝑇 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧))) → 𝑆 ∈ V) |
65 | 64 | a1i 11 |
. . 3
⊢ (𝜑 → (∃𝑠(𝑠 = 𝑆 ∧ (𝑠 ∈ 𝒫 𝑇 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧))) → 𝑆 ∈ V)) |
66 | | ssexg 5219 |
. . . . . 6
⊢ ((𝑆 ⊆ 𝑇 ∧ 𝑇 ∈ 𝑉) → 𝑆 ∈ V) |
67 | 66 | expcom 416 |
. . . . 5
⊢ (𝑇 ∈ 𝑉 → (𝑆 ⊆ 𝑇 → 𝑆 ∈ V)) |
68 | 22, 67 | syl 17 |
. . . 4
⊢ (𝜑 → (𝑆 ⊆ 𝑇 → 𝑆 ∈ V)) |
69 | 68 | adantrd 494 |
. . 3
⊢ (𝜑 → ((𝑆 ⊆ 𝑇 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥𝐻𝑦) ⊆ (𝑥𝐽𝑦)) → 𝑆 ∈ V)) |
70 | 31 | elpw 4545 |
. . . . . . 7
⊢ (𝑠 ∈ 𝒫 𝑇 ↔ 𝑠 ⊆ 𝑇) |
71 | | sseq1 3991 |
. . . . . . 7
⊢ (𝑠 = 𝑆 → (𝑠 ⊆ 𝑇 ↔ 𝑆 ⊆ 𝑇)) |
72 | 70, 71 | syl5bb 285 |
. . . . . 6
⊢ (𝑠 = 𝑆 → (𝑠 ∈ 𝒫 𝑇 ↔ 𝑆 ⊆ 𝑇)) |
73 | 51 | raleqdv 3415 |
. . . . . . 7
⊢ (𝑠 = 𝑆 → (∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧) ↔ ∀𝑧 ∈ (𝑆 × 𝑆)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧))) |
74 | | fvex 6677 |
. . . . . . . . . 10
⊢ (𝐻‘𝑧) ∈ V |
75 | 74 | elpw 4545 |
. . . . . . . . 9
⊢ ((𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧) ↔ (𝐻‘𝑧) ⊆ (𝐽‘𝑧)) |
76 | | fveq2 6664 |
. . . . . . . . . . 11
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (𝐻‘𝑧) = (𝐻‘〈𝑥, 𝑦〉)) |
77 | | df-ov 7153 |
. . . . . . . . . . 11
⊢ (𝑥𝐻𝑦) = (𝐻‘〈𝑥, 𝑦〉) |
78 | 76, 77 | syl6eqr 2874 |
. . . . . . . . . 10
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (𝐻‘𝑧) = (𝑥𝐻𝑦)) |
79 | | fveq2 6664 |
. . . . . . . . . . 11
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (𝐽‘𝑧) = (𝐽‘〈𝑥, 𝑦〉)) |
80 | | df-ov 7153 |
. . . . . . . . . . 11
⊢ (𝑥𝐽𝑦) = (𝐽‘〈𝑥, 𝑦〉) |
81 | 79, 80 | syl6eqr 2874 |
. . . . . . . . . 10
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (𝐽‘𝑧) = (𝑥𝐽𝑦)) |
82 | 78, 81 | sseq12d 3999 |
. . . . . . . . 9
⊢ (𝑧 = 〈𝑥, 𝑦〉 → ((𝐻‘𝑧) ⊆ (𝐽‘𝑧) ↔ (𝑥𝐻𝑦) ⊆ (𝑥𝐽𝑦))) |
83 | 75, 82 | syl5bb 285 |
. . . . . . . 8
⊢ (𝑧 = 〈𝑥, 𝑦〉 → ((𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧) ↔ (𝑥𝐻𝑦) ⊆ (𝑥𝐽𝑦))) |
84 | 83 | ralxp 5706 |
. . . . . . 7
⊢
(∀𝑧 ∈
(𝑆 × 𝑆)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧) ↔ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥𝐻𝑦) ⊆ (𝑥𝐽𝑦)) |
85 | 73, 84 | syl6bb 289 |
. . . . . 6
⊢ (𝑠 = 𝑆 → (∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧) ↔ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥𝐻𝑦) ⊆ (𝑥𝐽𝑦))) |
86 | 72, 85 | anbi12d 632 |
. . . . 5
⊢ (𝑠 = 𝑆 → ((𝑠 ∈ 𝒫 𝑇 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧)) ↔ (𝑆 ⊆ 𝑇 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥𝐻𝑦) ⊆ (𝑥𝐽𝑦)))) |
87 | 86 | ceqsexgv 3646 |
. . . 4
⊢ (𝑆 ∈ V → (∃𝑠(𝑠 = 𝑆 ∧ (𝑠 ∈ 𝒫 𝑇 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧))) ↔ (𝑆 ⊆ 𝑇 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥𝐻𝑦) ⊆ (𝑥𝐽𝑦)))) |
88 | 87 | a1i 11 |
. . 3
⊢ (𝜑 → (𝑆 ∈ V → (∃𝑠(𝑠 = 𝑆 ∧ (𝑠 ∈ 𝒫 𝑇 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧))) ↔ (𝑆 ⊆ 𝑇 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥𝐻𝑦) ⊆ (𝑥𝐽𝑦))))) |
89 | 65, 69, 88 | pm5.21ndd 383 |
. 2
⊢ (𝜑 → (∃𝑠(𝑠 = 𝑆 ∧ (𝑠 ∈ 𝒫 𝑇 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧))) ↔ (𝑆 ⊆ 𝑇 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥𝐻𝑦) ⊆ (𝑥𝐽𝑦)))) |
90 | 27, 61, 89 | 3bitrd 307 |
1
⊢ (𝜑 → (𝐻 ⊆cat 𝐽 ↔ (𝑆 ⊆ 𝑇 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥𝐻𝑦) ⊆ (𝑥𝐽𝑦)))) |