Step | Hyp | Ref
| Expression |
1 | | brssc 17526 |
. . . 4
⊢ (𝐻 ⊆cat 𝐽 ↔ ∃𝑡(𝐽 Fn (𝑡 × 𝑡) ∧ ∃𝑠 ∈ 𝒫 𝑡𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧))) |
2 | | fndm 6536 |
. . . . . . . . . . . 12
⊢ (𝐽 Fn (𝑡 × 𝑡) → dom 𝐽 = (𝑡 × 𝑡)) |
3 | 2 | adantl 482 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐽 Fn (𝑡 × 𝑡)) → dom 𝐽 = (𝑡 × 𝑡)) |
4 | | isssc.2 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐽 Fn (𝑇 × 𝑇)) |
5 | 4 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐽 Fn (𝑡 × 𝑡)) → 𝐽 Fn (𝑇 × 𝑇)) |
6 | 5 | fndmd 6538 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐽 Fn (𝑡 × 𝑡)) → dom 𝐽 = (𝑇 × 𝑇)) |
7 | 3, 6 | eqtr3d 2780 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐽 Fn (𝑡 × 𝑡)) → (𝑡 × 𝑡) = (𝑇 × 𝑇)) |
8 | 7 | dmeqd 5814 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐽 Fn (𝑡 × 𝑡)) → dom (𝑡 × 𝑡) = dom (𝑇 × 𝑇)) |
9 | | dmxpid 5839 |
. . . . . . . . 9
⊢ dom
(𝑡 × 𝑡) = 𝑡 |
10 | | dmxpid 5839 |
. . . . . . . . 9
⊢ dom
(𝑇 × 𝑇) = 𝑇 |
11 | 8, 9, 10 | 3eqtr3g 2801 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐽 Fn (𝑡 × 𝑡)) → 𝑡 = 𝑇) |
12 | 11 | ex 413 |
. . . . . . 7
⊢ (𝜑 → (𝐽 Fn (𝑡 × 𝑡) → 𝑡 = 𝑇)) |
13 | | id 22 |
. . . . . . . . . 10
⊢ (𝑡 = 𝑇 → 𝑡 = 𝑇) |
14 | 13 | sqxpeqd 5621 |
. . . . . . . . 9
⊢ (𝑡 = 𝑇 → (𝑡 × 𝑡) = (𝑇 × 𝑇)) |
15 | 14 | fneq2d 6527 |
. . . . . . . 8
⊢ (𝑡 = 𝑇 → (𝐽 Fn (𝑡 × 𝑡) ↔ 𝐽 Fn (𝑇 × 𝑇))) |
16 | 4, 15 | syl5ibrcom 246 |
. . . . . . 7
⊢ (𝜑 → (𝑡 = 𝑇 → 𝐽 Fn (𝑡 × 𝑡))) |
17 | 12, 16 | impbid 211 |
. . . . . 6
⊢ (𝜑 → (𝐽 Fn (𝑡 × 𝑡) ↔ 𝑡 = 𝑇)) |
18 | 17 | anbi1d 630 |
. . . . 5
⊢ (𝜑 → ((𝐽 Fn (𝑡 × 𝑡) ∧ ∃𝑠 ∈ 𝒫 𝑡𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧)) ↔ (𝑡 = 𝑇 ∧ ∃𝑠 ∈ 𝒫 𝑡𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧)))) |
19 | 18 | exbidv 1924 |
. . . 4
⊢ (𝜑 → (∃𝑡(𝐽 Fn (𝑡 × 𝑡) ∧ ∃𝑠 ∈ 𝒫 𝑡𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧)) ↔ ∃𝑡(𝑡 = 𝑇 ∧ ∃𝑠 ∈ 𝒫 𝑡𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧)))) |
20 | 1, 19 | bitrid 282 |
. . 3
⊢ (𝜑 → (𝐻 ⊆cat 𝐽 ↔ ∃𝑡(𝑡 = 𝑇 ∧ ∃𝑠 ∈ 𝒫 𝑡𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧)))) |
21 | | isssc.3 |
. . . 4
⊢ (𝜑 → 𝑇 ∈ 𝑉) |
22 | | pweq 4549 |
. . . . . 6
⊢ (𝑡 = 𝑇 → 𝒫 𝑡 = 𝒫 𝑇) |
23 | 22 | rexeqdv 3349 |
. . . . 5
⊢ (𝑡 = 𝑇 → (∃𝑠 ∈ 𝒫 𝑡𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧) ↔ ∃𝑠 ∈ 𝒫 𝑇𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧))) |
24 | 23 | ceqsexgv 3584 |
. . . 4
⊢ (𝑇 ∈ 𝑉 → (∃𝑡(𝑡 = 𝑇 ∧ ∃𝑠 ∈ 𝒫 𝑡𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧)) ↔ ∃𝑠 ∈ 𝒫 𝑇𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧))) |
25 | 21, 24 | syl 17 |
. . 3
⊢ (𝜑 → (∃𝑡(𝑡 = 𝑇 ∧ ∃𝑠 ∈ 𝒫 𝑡𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧)) ↔ ∃𝑠 ∈ 𝒫 𝑇𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧))) |
26 | 20, 25 | bitrd 278 |
. 2
⊢ (𝜑 → (𝐻 ⊆cat 𝐽 ↔ ∃𝑠 ∈ 𝒫 𝑇𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧))) |
27 | | df-rex 3070 |
. . 3
⊢
(∃𝑠 ∈
𝒫 𝑇𝐻 ∈ X𝑧 ∈
(𝑠 × 𝑠)𝒫 (𝐽‘𝑧) ↔ ∃𝑠(𝑠 ∈ 𝒫 𝑇 ∧ 𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧))) |
28 | | 3anass 1094 |
. . . . . . . 8
⊢ ((𝐻 ∈ V ∧ 𝐻 Fn (𝑠 × 𝑠) ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧)) ↔ (𝐻 ∈ V ∧ (𝐻 Fn (𝑠 × 𝑠) ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧)))) |
29 | | elixp2 8689 |
. . . . . . . 8
⊢ (𝐻 ∈ X𝑧 ∈
(𝑠 × 𝑠)𝒫 (𝐽‘𝑧) ↔ (𝐻 ∈ V ∧ 𝐻 Fn (𝑠 × 𝑠) ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧))) |
30 | | vex 3436 |
. . . . . . . . . . . 12
⊢ 𝑠 ∈ V |
31 | 30, 30 | xpex 7603 |
. . . . . . . . . . 11
⊢ (𝑠 × 𝑠) ∈ V |
32 | | fnex 7093 |
. . . . . . . . . . 11
⊢ ((𝐻 Fn (𝑠 × 𝑠) ∧ (𝑠 × 𝑠) ∈ V) → 𝐻 ∈ V) |
33 | 31, 32 | mpan2 688 |
. . . . . . . . . 10
⊢ (𝐻 Fn (𝑠 × 𝑠) → 𝐻 ∈ V) |
34 | 33 | adantr 481 |
. . . . . . . . 9
⊢ ((𝐻 Fn (𝑠 × 𝑠) ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧)) → 𝐻 ∈ V) |
35 | 34 | pm4.71ri 561 |
. . . . . . . 8
⊢ ((𝐻 Fn (𝑠 × 𝑠) ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧)) ↔ (𝐻 ∈ V ∧ (𝐻 Fn (𝑠 × 𝑠) ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧)))) |
36 | 28, 29, 35 | 3bitr4i 303 |
. . . . . . 7
⊢ (𝐻 ∈ X𝑧 ∈
(𝑠 × 𝑠)𝒫 (𝐽‘𝑧) ↔ (𝐻 Fn (𝑠 × 𝑠) ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧))) |
37 | | fndm 6536 |
. . . . . . . . . . . . . 14
⊢ (𝐻 Fn (𝑠 × 𝑠) → dom 𝐻 = (𝑠 × 𝑠)) |
38 | 37 | adantl 482 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐻 Fn (𝑠 × 𝑠)) → dom 𝐻 = (𝑠 × 𝑠)) |
39 | | isssc.1 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆)) |
40 | 39 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝐻 Fn (𝑠 × 𝑠)) → 𝐻 Fn (𝑆 × 𝑆)) |
41 | 40 | fndmd 6538 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐻 Fn (𝑠 × 𝑠)) → dom 𝐻 = (𝑆 × 𝑆)) |
42 | 38, 41 | eqtr3d 2780 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐻 Fn (𝑠 × 𝑠)) → (𝑠 × 𝑠) = (𝑆 × 𝑆)) |
43 | 42 | dmeqd 5814 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐻 Fn (𝑠 × 𝑠)) → dom (𝑠 × 𝑠) = dom (𝑆 × 𝑆)) |
44 | | dmxpid 5839 |
. . . . . . . . . . 11
⊢ dom
(𝑠 × 𝑠) = 𝑠 |
45 | | dmxpid 5839 |
. . . . . . . . . . 11
⊢ dom
(𝑆 × 𝑆) = 𝑆 |
46 | 43, 44, 45 | 3eqtr3g 2801 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐻 Fn (𝑠 × 𝑠)) → 𝑠 = 𝑆) |
47 | 46 | ex 413 |
. . . . . . . . 9
⊢ (𝜑 → (𝐻 Fn (𝑠 × 𝑠) → 𝑠 = 𝑆)) |
48 | | id 22 |
. . . . . . . . . . . 12
⊢ (𝑠 = 𝑆 → 𝑠 = 𝑆) |
49 | 48 | sqxpeqd 5621 |
. . . . . . . . . . 11
⊢ (𝑠 = 𝑆 → (𝑠 × 𝑠) = (𝑆 × 𝑆)) |
50 | 49 | fneq2d 6527 |
. . . . . . . . . 10
⊢ (𝑠 = 𝑆 → (𝐻 Fn (𝑠 × 𝑠) ↔ 𝐻 Fn (𝑆 × 𝑆))) |
51 | 39, 50 | syl5ibrcom 246 |
. . . . . . . . 9
⊢ (𝜑 → (𝑠 = 𝑆 → 𝐻 Fn (𝑠 × 𝑠))) |
52 | 47, 51 | impbid 211 |
. . . . . . . 8
⊢ (𝜑 → (𝐻 Fn (𝑠 × 𝑠) ↔ 𝑠 = 𝑆)) |
53 | 52 | anbi1d 630 |
. . . . . . 7
⊢ (𝜑 → ((𝐻 Fn (𝑠 × 𝑠) ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧)) ↔ (𝑠 = 𝑆 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧)))) |
54 | 36, 53 | bitrid 282 |
. . . . . 6
⊢ (𝜑 → (𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧) ↔ (𝑠 = 𝑆 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧)))) |
55 | 54 | anbi2d 629 |
. . . . 5
⊢ (𝜑 → ((𝑠 ∈ 𝒫 𝑇 ∧ 𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧)) ↔ (𝑠 ∈ 𝒫 𝑇 ∧ (𝑠 = 𝑆 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧))))) |
56 | | an12 642 |
. . . . 5
⊢ ((𝑠 ∈ 𝒫 𝑇 ∧ (𝑠 = 𝑆 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧))) ↔ (𝑠 = 𝑆 ∧ (𝑠 ∈ 𝒫 𝑇 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧)))) |
57 | 55, 56 | bitrdi 287 |
. . . 4
⊢ (𝜑 → ((𝑠 ∈ 𝒫 𝑇 ∧ 𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧)) ↔ (𝑠 = 𝑆 ∧ (𝑠 ∈ 𝒫 𝑇 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧))))) |
58 | 57 | exbidv 1924 |
. . 3
⊢ (𝜑 → (∃𝑠(𝑠 ∈ 𝒫 𝑇 ∧ 𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧)) ↔ ∃𝑠(𝑠 = 𝑆 ∧ (𝑠 ∈ 𝒫 𝑇 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧))))) |
59 | 27, 58 | bitrid 282 |
. 2
⊢ (𝜑 → (∃𝑠 ∈ 𝒫 𝑇𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧) ↔ ∃𝑠(𝑠 = 𝑆 ∧ (𝑠 ∈ 𝒫 𝑇 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧))))) |
60 | | exsimpl 1871 |
. . . . 5
⊢
(∃𝑠(𝑠 = 𝑆 ∧ (𝑠 ∈ 𝒫 𝑇 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧))) → ∃𝑠 𝑠 = 𝑆) |
61 | | isset 3445 |
. . . . 5
⊢ (𝑆 ∈ V ↔ ∃𝑠 𝑠 = 𝑆) |
62 | 60, 61 | sylibr 233 |
. . . 4
⊢
(∃𝑠(𝑠 = 𝑆 ∧ (𝑠 ∈ 𝒫 𝑇 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧))) → 𝑆 ∈ V) |
63 | 62 | a1i 11 |
. . 3
⊢ (𝜑 → (∃𝑠(𝑠 = 𝑆 ∧ (𝑠 ∈ 𝒫 𝑇 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧))) → 𝑆 ∈ V)) |
64 | | ssexg 5247 |
. . . . . 6
⊢ ((𝑆 ⊆ 𝑇 ∧ 𝑇 ∈ 𝑉) → 𝑆 ∈ V) |
65 | 64 | expcom 414 |
. . . . 5
⊢ (𝑇 ∈ 𝑉 → (𝑆 ⊆ 𝑇 → 𝑆 ∈ V)) |
66 | 21, 65 | syl 17 |
. . . 4
⊢ (𝜑 → (𝑆 ⊆ 𝑇 → 𝑆 ∈ V)) |
67 | 66 | adantrd 492 |
. . 3
⊢ (𝜑 → ((𝑆 ⊆ 𝑇 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥𝐻𝑦) ⊆ (𝑥𝐽𝑦)) → 𝑆 ∈ V)) |
68 | 30 | elpw 4537 |
. . . . . . 7
⊢ (𝑠 ∈ 𝒫 𝑇 ↔ 𝑠 ⊆ 𝑇) |
69 | | sseq1 3946 |
. . . . . . 7
⊢ (𝑠 = 𝑆 → (𝑠 ⊆ 𝑇 ↔ 𝑆 ⊆ 𝑇)) |
70 | 68, 69 | bitrid 282 |
. . . . . 6
⊢ (𝑠 = 𝑆 → (𝑠 ∈ 𝒫 𝑇 ↔ 𝑆 ⊆ 𝑇)) |
71 | 49 | raleqdv 3348 |
. . . . . . 7
⊢ (𝑠 = 𝑆 → (∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧) ↔ ∀𝑧 ∈ (𝑆 × 𝑆)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧))) |
72 | | fvex 6787 |
. . . . . . . . . 10
⊢ (𝐻‘𝑧) ∈ V |
73 | 72 | elpw 4537 |
. . . . . . . . 9
⊢ ((𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧) ↔ (𝐻‘𝑧) ⊆ (𝐽‘𝑧)) |
74 | | fveq2 6774 |
. . . . . . . . . . 11
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (𝐻‘𝑧) = (𝐻‘〈𝑥, 𝑦〉)) |
75 | | df-ov 7278 |
. . . . . . . . . . 11
⊢ (𝑥𝐻𝑦) = (𝐻‘〈𝑥, 𝑦〉) |
76 | 74, 75 | eqtr4di 2796 |
. . . . . . . . . 10
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (𝐻‘𝑧) = (𝑥𝐻𝑦)) |
77 | | fveq2 6774 |
. . . . . . . . . . 11
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (𝐽‘𝑧) = (𝐽‘〈𝑥, 𝑦〉)) |
78 | | df-ov 7278 |
. . . . . . . . . . 11
⊢ (𝑥𝐽𝑦) = (𝐽‘〈𝑥, 𝑦〉) |
79 | 77, 78 | eqtr4di 2796 |
. . . . . . . . . 10
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (𝐽‘𝑧) = (𝑥𝐽𝑦)) |
80 | 76, 79 | sseq12d 3954 |
. . . . . . . . 9
⊢ (𝑧 = 〈𝑥, 𝑦〉 → ((𝐻‘𝑧) ⊆ (𝐽‘𝑧) ↔ (𝑥𝐻𝑦) ⊆ (𝑥𝐽𝑦))) |
81 | 73, 80 | bitrid 282 |
. . . . . . . 8
⊢ (𝑧 = 〈𝑥, 𝑦〉 → ((𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧) ↔ (𝑥𝐻𝑦) ⊆ (𝑥𝐽𝑦))) |
82 | 81 | ralxp 5750 |
. . . . . . 7
⊢
(∀𝑧 ∈
(𝑆 × 𝑆)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧) ↔ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥𝐻𝑦) ⊆ (𝑥𝐽𝑦)) |
83 | 71, 82 | bitrdi 287 |
. . . . . 6
⊢ (𝑠 = 𝑆 → (∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧) ↔ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥𝐻𝑦) ⊆ (𝑥𝐽𝑦))) |
84 | 70, 83 | anbi12d 631 |
. . . . 5
⊢ (𝑠 = 𝑆 → ((𝑠 ∈ 𝒫 𝑇 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧)) ↔ (𝑆 ⊆ 𝑇 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥𝐻𝑦) ⊆ (𝑥𝐽𝑦)))) |
85 | 84 | ceqsexgv 3584 |
. . . 4
⊢ (𝑆 ∈ V → (∃𝑠(𝑠 = 𝑆 ∧ (𝑠 ∈ 𝒫 𝑇 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧))) ↔ (𝑆 ⊆ 𝑇 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥𝐻𝑦) ⊆ (𝑥𝐽𝑦)))) |
86 | 85 | a1i 11 |
. . 3
⊢ (𝜑 → (𝑆 ∈ V → (∃𝑠(𝑠 = 𝑆 ∧ (𝑠 ∈ 𝒫 𝑇 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧))) ↔ (𝑆 ⊆ 𝑇 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥𝐻𝑦) ⊆ (𝑥𝐽𝑦))))) |
87 | 63, 67, 86 | pm5.21ndd 381 |
. 2
⊢ (𝜑 → (∃𝑠(𝑠 = 𝑆 ∧ (𝑠 ∈ 𝒫 𝑇 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧))) ↔ (𝑆 ⊆ 𝑇 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥𝐻𝑦) ⊆ (𝑥𝐽𝑦)))) |
88 | 26, 59, 87 | 3bitrd 305 |
1
⊢ (𝜑 → (𝐻 ⊆cat 𝐽 ↔ (𝑆 ⊆ 𝑇 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥𝐻𝑦) ⊆ (𝑥𝐽𝑦)))) |