Step | Hyp | Ref
| Expression |
1 | | brssc 17189 |
. . . 4
⊢ (𝐻 ⊆cat 𝐽 ↔ ∃𝑡(𝐽 Fn (𝑡 × 𝑡) ∧ ∃𝑠 ∈ 𝒫 𝑡𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧))) |
2 | | fndm 6440 |
. . . . . . . . . . . 12
⊢ (𝐽 Fn (𝑡 × 𝑡) → dom 𝐽 = (𝑡 × 𝑡)) |
3 | 2 | adantl 485 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐽 Fn (𝑡 × 𝑡)) → dom 𝐽 = (𝑡 × 𝑡)) |
4 | | isssc.2 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐽 Fn (𝑇 × 𝑇)) |
5 | 4 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐽 Fn (𝑡 × 𝑡)) → 𝐽 Fn (𝑇 × 𝑇)) |
6 | 5 | fndmd 6442 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐽 Fn (𝑡 × 𝑡)) → dom 𝐽 = (𝑇 × 𝑇)) |
7 | 3, 6 | eqtr3d 2775 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐽 Fn (𝑡 × 𝑡)) → (𝑡 × 𝑡) = (𝑇 × 𝑇)) |
8 | 7 | dmeqd 5748 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐽 Fn (𝑡 × 𝑡)) → dom (𝑡 × 𝑡) = dom (𝑇 × 𝑇)) |
9 | | dmxpid 5773 |
. . . . . . . . 9
⊢ dom
(𝑡 × 𝑡) = 𝑡 |
10 | | dmxpid 5773 |
. . . . . . . . 9
⊢ dom
(𝑇 × 𝑇) = 𝑇 |
11 | 8, 9, 10 | 3eqtr3g 2796 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐽 Fn (𝑡 × 𝑡)) → 𝑡 = 𝑇) |
12 | 11 | ex 416 |
. . . . . . 7
⊢ (𝜑 → (𝐽 Fn (𝑡 × 𝑡) → 𝑡 = 𝑇)) |
13 | | id 22 |
. . . . . . . . . 10
⊢ (𝑡 = 𝑇 → 𝑡 = 𝑇) |
14 | 13 | sqxpeqd 5557 |
. . . . . . . . 9
⊢ (𝑡 = 𝑇 → (𝑡 × 𝑡) = (𝑇 × 𝑇)) |
15 | 14 | fneq2d 6432 |
. . . . . . . 8
⊢ (𝑡 = 𝑇 → (𝐽 Fn (𝑡 × 𝑡) ↔ 𝐽 Fn (𝑇 × 𝑇))) |
16 | 4, 15 | syl5ibrcom 250 |
. . . . . . 7
⊢ (𝜑 → (𝑡 = 𝑇 → 𝐽 Fn (𝑡 × 𝑡))) |
17 | 12, 16 | impbid 215 |
. . . . . 6
⊢ (𝜑 → (𝐽 Fn (𝑡 × 𝑡) ↔ 𝑡 = 𝑇)) |
18 | 17 | anbi1d 633 |
. . . . 5
⊢ (𝜑 → ((𝐽 Fn (𝑡 × 𝑡) ∧ ∃𝑠 ∈ 𝒫 𝑡𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧)) ↔ (𝑡 = 𝑇 ∧ ∃𝑠 ∈ 𝒫 𝑡𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧)))) |
19 | 18 | exbidv 1928 |
. . . 4
⊢ (𝜑 → (∃𝑡(𝐽 Fn (𝑡 × 𝑡) ∧ ∃𝑠 ∈ 𝒫 𝑡𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧)) ↔ ∃𝑡(𝑡 = 𝑇 ∧ ∃𝑠 ∈ 𝒫 𝑡𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧)))) |
20 | 1, 19 | syl5bb 286 |
. . 3
⊢ (𝜑 → (𝐻 ⊆cat 𝐽 ↔ ∃𝑡(𝑡 = 𝑇 ∧ ∃𝑠 ∈ 𝒫 𝑡𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧)))) |
21 | | isssc.3 |
. . . 4
⊢ (𝜑 → 𝑇 ∈ 𝑉) |
22 | | pweq 4504 |
. . . . . 6
⊢ (𝑡 = 𝑇 → 𝒫 𝑡 = 𝒫 𝑇) |
23 | 22 | rexeqdv 3317 |
. . . . 5
⊢ (𝑡 = 𝑇 → (∃𝑠 ∈ 𝒫 𝑡𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧) ↔ ∃𝑠 ∈ 𝒫 𝑇𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧))) |
24 | 23 | ceqsexgv 3550 |
. . . 4
⊢ (𝑇 ∈ 𝑉 → (∃𝑡(𝑡 = 𝑇 ∧ ∃𝑠 ∈ 𝒫 𝑡𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧)) ↔ ∃𝑠 ∈ 𝒫 𝑇𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧))) |
25 | 21, 24 | syl 17 |
. . 3
⊢ (𝜑 → (∃𝑡(𝑡 = 𝑇 ∧ ∃𝑠 ∈ 𝒫 𝑡𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧)) ↔ ∃𝑠 ∈ 𝒫 𝑇𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧))) |
26 | 20, 25 | bitrd 282 |
. 2
⊢ (𝜑 → (𝐻 ⊆cat 𝐽 ↔ ∃𝑠 ∈ 𝒫 𝑇𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧))) |
27 | | df-rex 3059 |
. . 3
⊢
(∃𝑠 ∈
𝒫 𝑇𝐻 ∈ X𝑧 ∈
(𝑠 × 𝑠)𝒫 (𝐽‘𝑧) ↔ ∃𝑠(𝑠 ∈ 𝒫 𝑇 ∧ 𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧))) |
28 | | 3anass 1096 |
. . . . . . . 8
⊢ ((𝐻 ∈ V ∧ 𝐻 Fn (𝑠 × 𝑠) ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧)) ↔ (𝐻 ∈ V ∧ (𝐻 Fn (𝑠 × 𝑠) ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧)))) |
29 | | elixp2 8511 |
. . . . . . . 8
⊢ (𝐻 ∈ X𝑧 ∈
(𝑠 × 𝑠)𝒫 (𝐽‘𝑧) ↔ (𝐻 ∈ V ∧ 𝐻 Fn (𝑠 × 𝑠) ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧))) |
30 | | vex 3402 |
. . . . . . . . . . . 12
⊢ 𝑠 ∈ V |
31 | 30, 30 | xpex 7494 |
. . . . . . . . . . 11
⊢ (𝑠 × 𝑠) ∈ V |
32 | | fnex 6990 |
. . . . . . . . . . 11
⊢ ((𝐻 Fn (𝑠 × 𝑠) ∧ (𝑠 × 𝑠) ∈ V) → 𝐻 ∈ V) |
33 | 31, 32 | mpan2 691 |
. . . . . . . . . 10
⊢ (𝐻 Fn (𝑠 × 𝑠) → 𝐻 ∈ V) |
34 | 33 | adantr 484 |
. . . . . . . . 9
⊢ ((𝐻 Fn (𝑠 × 𝑠) ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧)) → 𝐻 ∈ V) |
35 | 34 | pm4.71ri 564 |
. . . . . . . 8
⊢ ((𝐻 Fn (𝑠 × 𝑠) ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧)) ↔ (𝐻 ∈ V ∧ (𝐻 Fn (𝑠 × 𝑠) ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧)))) |
36 | 28, 29, 35 | 3bitr4i 306 |
. . . . . . 7
⊢ (𝐻 ∈ X𝑧 ∈
(𝑠 × 𝑠)𝒫 (𝐽‘𝑧) ↔ (𝐻 Fn (𝑠 × 𝑠) ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧))) |
37 | | fndm 6440 |
. . . . . . . . . . . . . 14
⊢ (𝐻 Fn (𝑠 × 𝑠) → dom 𝐻 = (𝑠 × 𝑠)) |
38 | 37 | adantl 485 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐻 Fn (𝑠 × 𝑠)) → dom 𝐻 = (𝑠 × 𝑠)) |
39 | | isssc.1 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆)) |
40 | 39 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝐻 Fn (𝑠 × 𝑠)) → 𝐻 Fn (𝑆 × 𝑆)) |
41 | 40 | fndmd 6442 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐻 Fn (𝑠 × 𝑠)) → dom 𝐻 = (𝑆 × 𝑆)) |
42 | 38, 41 | eqtr3d 2775 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐻 Fn (𝑠 × 𝑠)) → (𝑠 × 𝑠) = (𝑆 × 𝑆)) |
43 | 42 | dmeqd 5748 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐻 Fn (𝑠 × 𝑠)) → dom (𝑠 × 𝑠) = dom (𝑆 × 𝑆)) |
44 | | dmxpid 5773 |
. . . . . . . . . . 11
⊢ dom
(𝑠 × 𝑠) = 𝑠 |
45 | | dmxpid 5773 |
. . . . . . . . . . 11
⊢ dom
(𝑆 × 𝑆) = 𝑆 |
46 | 43, 44, 45 | 3eqtr3g 2796 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐻 Fn (𝑠 × 𝑠)) → 𝑠 = 𝑆) |
47 | 46 | ex 416 |
. . . . . . . . 9
⊢ (𝜑 → (𝐻 Fn (𝑠 × 𝑠) → 𝑠 = 𝑆)) |
48 | | id 22 |
. . . . . . . . . . . 12
⊢ (𝑠 = 𝑆 → 𝑠 = 𝑆) |
49 | 48 | sqxpeqd 5557 |
. . . . . . . . . . 11
⊢ (𝑠 = 𝑆 → (𝑠 × 𝑠) = (𝑆 × 𝑆)) |
50 | 49 | fneq2d 6432 |
. . . . . . . . . 10
⊢ (𝑠 = 𝑆 → (𝐻 Fn (𝑠 × 𝑠) ↔ 𝐻 Fn (𝑆 × 𝑆))) |
51 | 39, 50 | syl5ibrcom 250 |
. . . . . . . . 9
⊢ (𝜑 → (𝑠 = 𝑆 → 𝐻 Fn (𝑠 × 𝑠))) |
52 | 47, 51 | impbid 215 |
. . . . . . . 8
⊢ (𝜑 → (𝐻 Fn (𝑠 × 𝑠) ↔ 𝑠 = 𝑆)) |
53 | 52 | anbi1d 633 |
. . . . . . 7
⊢ (𝜑 → ((𝐻 Fn (𝑠 × 𝑠) ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧)) ↔ (𝑠 = 𝑆 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧)))) |
54 | 36, 53 | syl5bb 286 |
. . . . . 6
⊢ (𝜑 → (𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧) ↔ (𝑠 = 𝑆 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧)))) |
55 | 54 | anbi2d 632 |
. . . . 5
⊢ (𝜑 → ((𝑠 ∈ 𝒫 𝑇 ∧ 𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧)) ↔ (𝑠 ∈ 𝒫 𝑇 ∧ (𝑠 = 𝑆 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧))))) |
56 | | an12 645 |
. . . . 5
⊢ ((𝑠 ∈ 𝒫 𝑇 ∧ (𝑠 = 𝑆 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧))) ↔ (𝑠 = 𝑆 ∧ (𝑠 ∈ 𝒫 𝑇 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧)))) |
57 | 55, 56 | bitrdi 290 |
. . . 4
⊢ (𝜑 → ((𝑠 ∈ 𝒫 𝑇 ∧ 𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧)) ↔ (𝑠 = 𝑆 ∧ (𝑠 ∈ 𝒫 𝑇 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧))))) |
58 | 57 | exbidv 1928 |
. . 3
⊢ (𝜑 → (∃𝑠(𝑠 ∈ 𝒫 𝑇 ∧ 𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧)) ↔ ∃𝑠(𝑠 = 𝑆 ∧ (𝑠 ∈ 𝒫 𝑇 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧))))) |
59 | 27, 58 | syl5bb 286 |
. 2
⊢ (𝜑 → (∃𝑠 ∈ 𝒫 𝑇𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧) ↔ ∃𝑠(𝑠 = 𝑆 ∧ (𝑠 ∈ 𝒫 𝑇 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧))))) |
60 | | exsimpl 1875 |
. . . . 5
⊢
(∃𝑠(𝑠 = 𝑆 ∧ (𝑠 ∈ 𝒫 𝑇 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧))) → ∃𝑠 𝑠 = 𝑆) |
61 | | isset 3411 |
. . . . 5
⊢ (𝑆 ∈ V ↔ ∃𝑠 𝑠 = 𝑆) |
62 | 60, 61 | sylibr 237 |
. . . 4
⊢
(∃𝑠(𝑠 = 𝑆 ∧ (𝑠 ∈ 𝒫 𝑇 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧))) → 𝑆 ∈ V) |
63 | 62 | a1i 11 |
. . 3
⊢ (𝜑 → (∃𝑠(𝑠 = 𝑆 ∧ (𝑠 ∈ 𝒫 𝑇 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧))) → 𝑆 ∈ V)) |
64 | | ssexg 5191 |
. . . . . 6
⊢ ((𝑆 ⊆ 𝑇 ∧ 𝑇 ∈ 𝑉) → 𝑆 ∈ V) |
65 | 64 | expcom 417 |
. . . . 5
⊢ (𝑇 ∈ 𝑉 → (𝑆 ⊆ 𝑇 → 𝑆 ∈ V)) |
66 | 21, 65 | syl 17 |
. . . 4
⊢ (𝜑 → (𝑆 ⊆ 𝑇 → 𝑆 ∈ V)) |
67 | 66 | adantrd 495 |
. . 3
⊢ (𝜑 → ((𝑆 ⊆ 𝑇 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥𝐻𝑦) ⊆ (𝑥𝐽𝑦)) → 𝑆 ∈ V)) |
68 | 30 | elpw 4492 |
. . . . . . 7
⊢ (𝑠 ∈ 𝒫 𝑇 ↔ 𝑠 ⊆ 𝑇) |
69 | | sseq1 3902 |
. . . . . . 7
⊢ (𝑠 = 𝑆 → (𝑠 ⊆ 𝑇 ↔ 𝑆 ⊆ 𝑇)) |
70 | 68, 69 | syl5bb 286 |
. . . . . 6
⊢ (𝑠 = 𝑆 → (𝑠 ∈ 𝒫 𝑇 ↔ 𝑆 ⊆ 𝑇)) |
71 | 49 | raleqdv 3316 |
. . . . . . 7
⊢ (𝑠 = 𝑆 → (∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧) ↔ ∀𝑧 ∈ (𝑆 × 𝑆)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧))) |
72 | | fvex 6687 |
. . . . . . . . . 10
⊢ (𝐻‘𝑧) ∈ V |
73 | 72 | elpw 4492 |
. . . . . . . . 9
⊢ ((𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧) ↔ (𝐻‘𝑧) ⊆ (𝐽‘𝑧)) |
74 | | fveq2 6674 |
. . . . . . . . . . 11
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (𝐻‘𝑧) = (𝐻‘〈𝑥, 𝑦〉)) |
75 | | df-ov 7173 |
. . . . . . . . . . 11
⊢ (𝑥𝐻𝑦) = (𝐻‘〈𝑥, 𝑦〉) |
76 | 74, 75 | eqtr4di 2791 |
. . . . . . . . . 10
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (𝐻‘𝑧) = (𝑥𝐻𝑦)) |
77 | | fveq2 6674 |
. . . . . . . . . . 11
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (𝐽‘𝑧) = (𝐽‘〈𝑥, 𝑦〉)) |
78 | | df-ov 7173 |
. . . . . . . . . . 11
⊢ (𝑥𝐽𝑦) = (𝐽‘〈𝑥, 𝑦〉) |
79 | 77, 78 | eqtr4di 2791 |
. . . . . . . . . 10
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (𝐽‘𝑧) = (𝑥𝐽𝑦)) |
80 | 76, 79 | sseq12d 3910 |
. . . . . . . . 9
⊢ (𝑧 = 〈𝑥, 𝑦〉 → ((𝐻‘𝑧) ⊆ (𝐽‘𝑧) ↔ (𝑥𝐻𝑦) ⊆ (𝑥𝐽𝑦))) |
81 | 73, 80 | syl5bb 286 |
. . . . . . . 8
⊢ (𝑧 = 〈𝑥, 𝑦〉 → ((𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧) ↔ (𝑥𝐻𝑦) ⊆ (𝑥𝐽𝑦))) |
82 | 81 | ralxp 5684 |
. . . . . . 7
⊢
(∀𝑧 ∈
(𝑆 × 𝑆)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧) ↔ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥𝐻𝑦) ⊆ (𝑥𝐽𝑦)) |
83 | 71, 82 | bitrdi 290 |
. . . . . 6
⊢ (𝑠 = 𝑆 → (∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧) ↔ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥𝐻𝑦) ⊆ (𝑥𝐽𝑦))) |
84 | 70, 83 | anbi12d 634 |
. . . . 5
⊢ (𝑠 = 𝑆 → ((𝑠 ∈ 𝒫 𝑇 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧)) ↔ (𝑆 ⊆ 𝑇 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥𝐻𝑦) ⊆ (𝑥𝐽𝑦)))) |
85 | 84 | ceqsexgv 3550 |
. . . 4
⊢ (𝑆 ∈ V → (∃𝑠(𝑠 = 𝑆 ∧ (𝑠 ∈ 𝒫 𝑇 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧))) ↔ (𝑆 ⊆ 𝑇 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥𝐻𝑦) ⊆ (𝑥𝐽𝑦)))) |
86 | 85 | a1i 11 |
. . 3
⊢ (𝜑 → (𝑆 ∈ V → (∃𝑠(𝑠 = 𝑆 ∧ (𝑠 ∈ 𝒫 𝑇 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧))) ↔ (𝑆 ⊆ 𝑇 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥𝐻𝑦) ⊆ (𝑥𝐽𝑦))))) |
87 | 63, 67, 86 | pm5.21ndd 384 |
. 2
⊢ (𝜑 → (∃𝑠(𝑠 = 𝑆 ∧ (𝑠 ∈ 𝒫 𝑇 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧))) ↔ (𝑆 ⊆ 𝑇 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥𝐻𝑦) ⊆ (𝑥𝐽𝑦)))) |
88 | 26, 59, 87 | 3bitrd 308 |
1
⊢ (𝜑 → (𝐻 ⊆cat 𝐽 ↔ (𝑆 ⊆ 𝑇 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥𝐻𝑦) ⊆ (𝑥𝐽𝑦)))) |