Step | Hyp | Ref
| Expression |
1 | | brssc 16297 |
. . . 4
⊢ (𝐻 ⊆cat 𝐽 ↔ ∃𝑡(𝐽 Fn (𝑡 × 𝑡) ∧ ∃𝑠 ∈ 𝒫 𝑡𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧))) |
2 | | fndm 5904 |
. . . . . . . . . . . 12
⊢ (𝐽 Fn (𝑡 × 𝑡) → dom 𝐽 = (𝑡 × 𝑡)) |
3 | 2 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐽 Fn (𝑡 × 𝑡)) → dom 𝐽 = (𝑡 × 𝑡)) |
4 | | isssc.2 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐽 Fn (𝑇 × 𝑇)) |
5 | 4 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐽 Fn (𝑡 × 𝑡)) → 𝐽 Fn (𝑇 × 𝑇)) |
6 | | fndm 5904 |
. . . . . . . . . . . 12
⊢ (𝐽 Fn (𝑇 × 𝑇) → dom 𝐽 = (𝑇 × 𝑇)) |
7 | 5, 6 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐽 Fn (𝑡 × 𝑡)) → dom 𝐽 = (𝑇 × 𝑇)) |
8 | 3, 7 | eqtr3d 2646 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐽 Fn (𝑡 × 𝑡)) → (𝑡 × 𝑡) = (𝑇 × 𝑇)) |
9 | 8 | dmeqd 5248 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐽 Fn (𝑡 × 𝑡)) → dom (𝑡 × 𝑡) = dom (𝑇 × 𝑇)) |
10 | | dmxpid 5266 |
. . . . . . . . 9
⊢ dom
(𝑡 × 𝑡) = 𝑡 |
11 | | dmxpid 5266 |
. . . . . . . . 9
⊢ dom
(𝑇 × 𝑇) = 𝑇 |
12 | 9, 10, 11 | 3eqtr3g 2667 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐽 Fn (𝑡 × 𝑡)) → 𝑡 = 𝑇) |
13 | 12 | ex 449 |
. . . . . . 7
⊢ (𝜑 → (𝐽 Fn (𝑡 × 𝑡) → 𝑡 = 𝑇)) |
14 | | id 22 |
. . . . . . . . . 10
⊢ (𝑡 = 𝑇 → 𝑡 = 𝑇) |
15 | 14 | sqxpeqd 5065 |
. . . . . . . . 9
⊢ (𝑡 = 𝑇 → (𝑡 × 𝑡) = (𝑇 × 𝑇)) |
16 | 15 | fneq2d 5896 |
. . . . . . . 8
⊢ (𝑡 = 𝑇 → (𝐽 Fn (𝑡 × 𝑡) ↔ 𝐽 Fn (𝑇 × 𝑇))) |
17 | 4, 16 | syl5ibrcom 236 |
. . . . . . 7
⊢ (𝜑 → (𝑡 = 𝑇 → 𝐽 Fn (𝑡 × 𝑡))) |
18 | 13, 17 | impbid 201 |
. . . . . 6
⊢ (𝜑 → (𝐽 Fn (𝑡 × 𝑡) ↔ 𝑡 = 𝑇)) |
19 | 18 | anbi1d 737 |
. . . . 5
⊢ (𝜑 → ((𝐽 Fn (𝑡 × 𝑡) ∧ ∃𝑠 ∈ 𝒫 𝑡𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧)) ↔ (𝑡 = 𝑇 ∧ ∃𝑠 ∈ 𝒫 𝑡𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧)))) |
20 | 19 | exbidv 1837 |
. . . 4
⊢ (𝜑 → (∃𝑡(𝐽 Fn (𝑡 × 𝑡) ∧ ∃𝑠 ∈ 𝒫 𝑡𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧)) ↔ ∃𝑡(𝑡 = 𝑇 ∧ ∃𝑠 ∈ 𝒫 𝑡𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧)))) |
21 | 1, 20 | syl5bb 271 |
. . 3
⊢ (𝜑 → (𝐻 ⊆cat 𝐽 ↔ ∃𝑡(𝑡 = 𝑇 ∧ ∃𝑠 ∈ 𝒫 𝑡𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧)))) |
22 | | isssc.3 |
. . . 4
⊢ (𝜑 → 𝑇 ∈ 𝑉) |
23 | | pweq 4111 |
. . . . . 6
⊢ (𝑡 = 𝑇 → 𝒫 𝑡 = 𝒫 𝑇) |
24 | 23 | rexeqdv 3122 |
. . . . 5
⊢ (𝑡 = 𝑇 → (∃𝑠 ∈ 𝒫 𝑡𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧) ↔ ∃𝑠 ∈ 𝒫 𝑇𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧))) |
25 | 24 | ceqsexgv 3305 |
. . . 4
⊢ (𝑇 ∈ 𝑉 → (∃𝑡(𝑡 = 𝑇 ∧ ∃𝑠 ∈ 𝒫 𝑡𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧)) ↔ ∃𝑠 ∈ 𝒫 𝑇𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧))) |
26 | 22, 25 | syl 17 |
. . 3
⊢ (𝜑 → (∃𝑡(𝑡 = 𝑇 ∧ ∃𝑠 ∈ 𝒫 𝑡𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧)) ↔ ∃𝑠 ∈ 𝒫 𝑇𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧))) |
27 | 21, 26 | bitrd 267 |
. 2
⊢ (𝜑 → (𝐻 ⊆cat 𝐽 ↔ ∃𝑠 ∈ 𝒫 𝑇𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧))) |
28 | | df-rex 2902 |
. . 3
⊢
(∃𝑠 ∈
𝒫 𝑇𝐻 ∈ X𝑧 ∈
(𝑠 × 𝑠)𝒫 (𝐽‘𝑧) ↔ ∃𝑠(𝑠 ∈ 𝒫 𝑇 ∧ 𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧))) |
29 | | 3anass 1035 |
. . . . . . . 8
⊢ ((𝐻 ∈ V ∧ 𝐻 Fn (𝑠 × 𝑠) ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧)) ↔ (𝐻 ∈ V ∧ (𝐻 Fn (𝑠 × 𝑠) ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧)))) |
30 | | elixp2 7798 |
. . . . . . . 8
⊢ (𝐻 ∈ X𝑧 ∈
(𝑠 × 𝑠)𝒫 (𝐽‘𝑧) ↔ (𝐻 ∈ V ∧ 𝐻 Fn (𝑠 × 𝑠) ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧))) |
31 | | vex 3176 |
. . . . . . . . . . . 12
⊢ 𝑠 ∈ V |
32 | 31, 31 | xpex 6860 |
. . . . . . . . . . 11
⊢ (𝑠 × 𝑠) ∈ V |
33 | | fnex 6386 |
. . . . . . . . . . 11
⊢ ((𝐻 Fn (𝑠 × 𝑠) ∧ (𝑠 × 𝑠) ∈ V) → 𝐻 ∈ V) |
34 | 32, 33 | mpan2 703 |
. . . . . . . . . 10
⊢ (𝐻 Fn (𝑠 × 𝑠) → 𝐻 ∈ V) |
35 | 34 | adantr 480 |
. . . . . . . . 9
⊢ ((𝐻 Fn (𝑠 × 𝑠) ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧)) → 𝐻 ∈ V) |
36 | 35 | pm4.71ri 663 |
. . . . . . . 8
⊢ ((𝐻 Fn (𝑠 × 𝑠) ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧)) ↔ (𝐻 ∈ V ∧ (𝐻 Fn (𝑠 × 𝑠) ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧)))) |
37 | 29, 30, 36 | 3bitr4i 291 |
. . . . . . 7
⊢ (𝐻 ∈ X𝑧 ∈
(𝑠 × 𝑠)𝒫 (𝐽‘𝑧) ↔ (𝐻 Fn (𝑠 × 𝑠) ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧))) |
38 | | fndm 5904 |
. . . . . . . . . . . . . 14
⊢ (𝐻 Fn (𝑠 × 𝑠) → dom 𝐻 = (𝑠 × 𝑠)) |
39 | 38 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐻 Fn (𝑠 × 𝑠)) → dom 𝐻 = (𝑠 × 𝑠)) |
40 | | isssc.1 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆)) |
41 | 40 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝐻 Fn (𝑠 × 𝑠)) → 𝐻 Fn (𝑆 × 𝑆)) |
42 | | fndm 5904 |
. . . . . . . . . . . . . 14
⊢ (𝐻 Fn (𝑆 × 𝑆) → dom 𝐻 = (𝑆 × 𝑆)) |
43 | 41, 42 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐻 Fn (𝑠 × 𝑠)) → dom 𝐻 = (𝑆 × 𝑆)) |
44 | 39, 43 | eqtr3d 2646 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐻 Fn (𝑠 × 𝑠)) → (𝑠 × 𝑠) = (𝑆 × 𝑆)) |
45 | 44 | dmeqd 5248 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐻 Fn (𝑠 × 𝑠)) → dom (𝑠 × 𝑠) = dom (𝑆 × 𝑆)) |
46 | | dmxpid 5266 |
. . . . . . . . . . 11
⊢ dom
(𝑠 × 𝑠) = 𝑠 |
47 | | dmxpid 5266 |
. . . . . . . . . . 11
⊢ dom
(𝑆 × 𝑆) = 𝑆 |
48 | 45, 46, 47 | 3eqtr3g 2667 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐻 Fn (𝑠 × 𝑠)) → 𝑠 = 𝑆) |
49 | 48 | ex 449 |
. . . . . . . . 9
⊢ (𝜑 → (𝐻 Fn (𝑠 × 𝑠) → 𝑠 = 𝑆)) |
50 | | id 22 |
. . . . . . . . . . . 12
⊢ (𝑠 = 𝑆 → 𝑠 = 𝑆) |
51 | 50 | sqxpeqd 5065 |
. . . . . . . . . . 11
⊢ (𝑠 = 𝑆 → (𝑠 × 𝑠) = (𝑆 × 𝑆)) |
52 | 51 | fneq2d 5896 |
. . . . . . . . . 10
⊢ (𝑠 = 𝑆 → (𝐻 Fn (𝑠 × 𝑠) ↔ 𝐻 Fn (𝑆 × 𝑆))) |
53 | 40, 52 | syl5ibrcom 236 |
. . . . . . . . 9
⊢ (𝜑 → (𝑠 = 𝑆 → 𝐻 Fn (𝑠 × 𝑠))) |
54 | 49, 53 | impbid 201 |
. . . . . . . 8
⊢ (𝜑 → (𝐻 Fn (𝑠 × 𝑠) ↔ 𝑠 = 𝑆)) |
55 | 54 | anbi1d 737 |
. . . . . . 7
⊢ (𝜑 → ((𝐻 Fn (𝑠 × 𝑠) ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧)) ↔ (𝑠 = 𝑆 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧)))) |
56 | 37, 55 | syl5bb 271 |
. . . . . 6
⊢ (𝜑 → (𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧) ↔ (𝑠 = 𝑆 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧)))) |
57 | 56 | anbi2d 736 |
. . . . 5
⊢ (𝜑 → ((𝑠 ∈ 𝒫 𝑇 ∧ 𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧)) ↔ (𝑠 ∈ 𝒫 𝑇 ∧ (𝑠 = 𝑆 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧))))) |
58 | | an12 834 |
. . . . 5
⊢ ((𝑠 ∈ 𝒫 𝑇 ∧ (𝑠 = 𝑆 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧))) ↔ (𝑠 = 𝑆 ∧ (𝑠 ∈ 𝒫 𝑇 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧)))) |
59 | 57, 58 | syl6bb 275 |
. . . 4
⊢ (𝜑 → ((𝑠 ∈ 𝒫 𝑇 ∧ 𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧)) ↔ (𝑠 = 𝑆 ∧ (𝑠 ∈ 𝒫 𝑇 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧))))) |
60 | 59 | exbidv 1837 |
. . 3
⊢ (𝜑 → (∃𝑠(𝑠 ∈ 𝒫 𝑇 ∧ 𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧)) ↔ ∃𝑠(𝑠 = 𝑆 ∧ (𝑠 ∈ 𝒫 𝑇 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧))))) |
61 | 28, 60 | syl5bb 271 |
. 2
⊢ (𝜑 → (∃𝑠 ∈ 𝒫 𝑇𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧) ↔ ∃𝑠(𝑠 = 𝑆 ∧ (𝑠 ∈ 𝒫 𝑇 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧))))) |
62 | | exsimpl 1783 |
. . . . 5
⊢
(∃𝑠(𝑠 = 𝑆 ∧ (𝑠 ∈ 𝒫 𝑇 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧))) → ∃𝑠 𝑠 = 𝑆) |
63 | | isset 3180 |
. . . . 5
⊢ (𝑆 ∈ V ↔ ∃𝑠 𝑠 = 𝑆) |
64 | 62, 63 | sylibr 223 |
. . . 4
⊢
(∃𝑠(𝑠 = 𝑆 ∧ (𝑠 ∈ 𝒫 𝑇 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧))) → 𝑆 ∈ V) |
65 | 64 | a1i 11 |
. . 3
⊢ (𝜑 → (∃𝑠(𝑠 = 𝑆 ∧ (𝑠 ∈ 𝒫 𝑇 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧))) → 𝑆 ∈ V)) |
66 | | ssexg 4732 |
. . . . . 6
⊢ ((𝑆 ⊆ 𝑇 ∧ 𝑇 ∈ 𝑉) → 𝑆 ∈ V) |
67 | 66 | expcom 450 |
. . . . 5
⊢ (𝑇 ∈ 𝑉 → (𝑆 ⊆ 𝑇 → 𝑆 ∈ V)) |
68 | 22, 67 | syl 17 |
. . . 4
⊢ (𝜑 → (𝑆 ⊆ 𝑇 → 𝑆 ∈ V)) |
69 | 68 | adantrd 483 |
. . 3
⊢ (𝜑 → ((𝑆 ⊆ 𝑇 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥𝐻𝑦) ⊆ (𝑥𝐽𝑦)) → 𝑆 ∈ V)) |
70 | 31 | elpw 4114 |
. . . . . . 7
⊢ (𝑠 ∈ 𝒫 𝑇 ↔ 𝑠 ⊆ 𝑇) |
71 | | sseq1 3589 |
. . . . . . 7
⊢ (𝑠 = 𝑆 → (𝑠 ⊆ 𝑇 ↔ 𝑆 ⊆ 𝑇)) |
72 | 70, 71 | syl5bb 271 |
. . . . . 6
⊢ (𝑠 = 𝑆 → (𝑠 ∈ 𝒫 𝑇 ↔ 𝑆 ⊆ 𝑇)) |
73 | 51 | raleqdv 3121 |
. . . . . . 7
⊢ (𝑠 = 𝑆 → (∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧) ↔ ∀𝑧 ∈ (𝑆 × 𝑆)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧))) |
74 | | fvex 6113 |
. . . . . . . . . 10
⊢ (𝐻‘𝑧) ∈ V |
75 | 74 | elpw 4114 |
. . . . . . . . 9
⊢ ((𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧) ↔ (𝐻‘𝑧) ⊆ (𝐽‘𝑧)) |
76 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (𝐻‘𝑧) = (𝐻‘〈𝑥, 𝑦〉)) |
77 | | df-ov 6552 |
. . . . . . . . . . 11
⊢ (𝑥𝐻𝑦) = (𝐻‘〈𝑥, 𝑦〉) |
78 | 76, 77 | syl6eqr 2662 |
. . . . . . . . . 10
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (𝐻‘𝑧) = (𝑥𝐻𝑦)) |
79 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (𝐽‘𝑧) = (𝐽‘〈𝑥, 𝑦〉)) |
80 | | df-ov 6552 |
. . . . . . . . . . 11
⊢ (𝑥𝐽𝑦) = (𝐽‘〈𝑥, 𝑦〉) |
81 | 79, 80 | syl6eqr 2662 |
. . . . . . . . . 10
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (𝐽‘𝑧) = (𝑥𝐽𝑦)) |
82 | 78, 81 | sseq12d 3597 |
. . . . . . . . 9
⊢ (𝑧 = 〈𝑥, 𝑦〉 → ((𝐻‘𝑧) ⊆ (𝐽‘𝑧) ↔ (𝑥𝐻𝑦) ⊆ (𝑥𝐽𝑦))) |
83 | 75, 82 | syl5bb 271 |
. . . . . . . 8
⊢ (𝑧 = 〈𝑥, 𝑦〉 → ((𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧) ↔ (𝑥𝐻𝑦) ⊆ (𝑥𝐽𝑦))) |
84 | 83 | ralxp 5185 |
. . . . . . 7
⊢
(∀𝑧 ∈
(𝑆 × 𝑆)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧) ↔ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥𝐻𝑦) ⊆ (𝑥𝐽𝑦)) |
85 | 73, 84 | syl6bb 275 |
. . . . . 6
⊢ (𝑠 = 𝑆 → (∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧) ↔ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥𝐻𝑦) ⊆ (𝑥𝐽𝑦))) |
86 | 72, 85 | anbi12d 743 |
. . . . 5
⊢ (𝑠 = 𝑆 → ((𝑠 ∈ 𝒫 𝑇 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧)) ↔ (𝑆 ⊆ 𝑇 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥𝐻𝑦) ⊆ (𝑥𝐽𝑦)))) |
87 | 86 | ceqsexgv 3305 |
. . . 4
⊢ (𝑆 ∈ V → (∃𝑠(𝑠 = 𝑆 ∧ (𝑠 ∈ 𝒫 𝑇 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧))) ↔ (𝑆 ⊆ 𝑇 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥𝐻𝑦) ⊆ (𝑥𝐽𝑦)))) |
88 | 87 | a1i 11 |
. . 3
⊢ (𝜑 → (𝑆 ∈ V → (∃𝑠(𝑠 = 𝑆 ∧ (𝑠 ∈ 𝒫 𝑇 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧))) ↔ (𝑆 ⊆ 𝑇 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥𝐻𝑦) ⊆ (𝑥𝐽𝑦))))) |
89 | 65, 69, 88 | pm5.21ndd 368 |
. 2
⊢ (𝜑 → (∃𝑠(𝑠 = 𝑆 ∧ (𝑠 ∈ 𝒫 𝑇 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧))) ↔ (𝑆 ⊆ 𝑇 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥𝐻𝑦) ⊆ (𝑥𝐽𝑦)))) |
90 | 27, 61, 89 | 3bitrd 293 |
1
⊢ (𝜑 → (𝐻 ⊆cat 𝐽 ↔ (𝑆 ⊆ 𝑇 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥𝐻𝑦) ⊆ (𝑥𝐽𝑦)))) |