Proof of Theorem cat1
Step | Hyp | Ref
| Expression |
1 | | 2on 8151 |
. . 3
⊢
2o ∈ On |
2 | | eqid 2739 |
. . . 4
⊢
(SetCat‘2o) =
(SetCat‘2o) |
3 | 2 | setccat 17469 |
. . 3
⊢
(2o ∈ On → (SetCat‘2o) ∈
Cat) |
4 | 1, 3 | ax-mp 5 |
. 2
⊢
(SetCat‘2o) ∈ Cat |
5 | 1 | a1i 11 |
. . . 4
⊢ (⊤
→ 2o ∈ On) |
6 | | eqid 2739 |
. . . 4
⊢
(Base‘(SetCat‘2o)) =
(Base‘(SetCat‘2o)) |
7 | | eqid 2739 |
. . . 4
⊢ (Hom
‘(SetCat‘2o)) = (Hom
‘(SetCat‘2o)) |
8 | | 0ex 5185 |
. . . . . . 7
⊢ ∅
∈ V |
9 | 8 | prid1 4663 |
. . . . . 6
⊢ ∅
∈ {∅, {∅}} |
10 | | df2o2 8159 |
. . . . . 6
⊢
2o = {∅, {∅}} |
11 | 9, 10 | eleqtrri 2833 |
. . . . 5
⊢ ∅
∈ 2o |
12 | 11 | a1i 11 |
. . . 4
⊢ (⊤
→ ∅ ∈ 2o) |
13 | | p0ex 5261 |
. . . . . . 7
⊢ {∅}
∈ V |
14 | 13 | prid2 4664 |
. . . . . 6
⊢ {∅}
∈ {∅, {∅}} |
15 | 14, 10 | eleqtrri 2833 |
. . . . 5
⊢ {∅}
∈ 2o |
16 | 15 | a1i 11 |
. . . 4
⊢ (⊤
→ {∅} ∈ 2o) |
17 | | 0nep0 5234 |
. . . . 5
⊢ ∅
≠ {∅} |
18 | 17 | a1i 11 |
. . . 4
⊢ (⊤
→ ∅ ≠ {∅}) |
19 | 2, 5, 6, 7, 12, 16, 18 | cat1lem 17480 |
. . 3
⊢ (⊤
→ ∃𝑥 ∈
(Base‘(SetCat‘2o))∃𝑦 ∈
(Base‘(SetCat‘2o))∃𝑧 ∈
(Base‘(SetCat‘2o))∃𝑤 ∈
(Base‘(SetCat‘2o))(((𝑥(Hom
‘(SetCat‘2o))𝑦) ∩ (𝑧(Hom
‘(SetCat‘2o))𝑤)) ≠ ∅ ∧ ¬ (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))) |
20 | 19 | mptru 1549 |
. 2
⊢
∃𝑥 ∈
(Base‘(SetCat‘2o))∃𝑦 ∈
(Base‘(SetCat‘2o))∃𝑧 ∈
(Base‘(SetCat‘2o))∃𝑤 ∈
(Base‘(SetCat‘2o))(((𝑥(Hom
‘(SetCat‘2o))𝑦) ∩ (𝑧(Hom
‘(SetCat‘2o))𝑤)) ≠ ∅ ∧ ¬ (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) |
21 | | fvexd 6701 |
. . . 4
⊢ (𝑐 = (SetCat‘2o)
→ (Base‘𝑐)
∈ V) |
22 | | fveq2 6686 |
. . . 4
⊢ (𝑐 = (SetCat‘2o)
→ (Base‘𝑐) =
(Base‘(SetCat‘2o))) |
23 | | fvexd 6701 |
. . . . 5
⊢ ((𝑐 = (SetCat‘2o)
∧ 𝑏 =
(Base‘(SetCat‘2o))) → (Hom ‘𝑐) ∈ V) |
24 | | fveq2 6686 |
. . . . . 6
⊢ (𝑐 = (SetCat‘2o)
→ (Hom ‘𝑐) =
(Hom ‘(SetCat‘2o))) |
25 | 24 | adantr 484 |
. . . . 5
⊢ ((𝑐 = (SetCat‘2o)
∧ 𝑏 =
(Base‘(SetCat‘2o))) → (Hom ‘𝑐) = (Hom
‘(SetCat‘2o))) |
26 | | oveq 7188 |
. . . . . . . . . . . 12
⊢ (ℎ = (Hom
‘(SetCat‘2o)) → (𝑥ℎ𝑦) = (𝑥(Hom
‘(SetCat‘2o))𝑦)) |
27 | | oveq 7188 |
. . . . . . . . . . . 12
⊢ (ℎ = (Hom
‘(SetCat‘2o)) → (𝑧ℎ𝑤) = (𝑧(Hom
‘(SetCat‘2o))𝑤)) |
28 | 26, 27 | ineq12d 4114 |
. . . . . . . . . . 11
⊢ (ℎ = (Hom
‘(SetCat‘2o)) → ((𝑥ℎ𝑦) ∩ (𝑧ℎ𝑤)) = ((𝑥(Hom
‘(SetCat‘2o))𝑦) ∩ (𝑧(Hom
‘(SetCat‘2o))𝑤))) |
29 | 28 | neeq1d 2994 |
. . . . . . . . . 10
⊢ (ℎ = (Hom
‘(SetCat‘2o)) → (((𝑥ℎ𝑦) ∩ (𝑧ℎ𝑤)) ≠ ∅ ↔ ((𝑥(Hom
‘(SetCat‘2o))𝑦) ∩ (𝑧(Hom
‘(SetCat‘2o))𝑤)) ≠ ∅)) |
30 | 29 | anbi1d 633 |
. . . . . . . . 9
⊢ (ℎ = (Hom
‘(SetCat‘2o)) → ((((𝑥ℎ𝑦) ∩ (𝑧ℎ𝑤)) ≠ ∅ ∧ ¬ (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ (((𝑥(Hom
‘(SetCat‘2o))𝑦) ∩ (𝑧(Hom
‘(SetCat‘2o))𝑤)) ≠ ∅ ∧ ¬ (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))) |
31 | 30 | 2rexbidv 3211 |
. . . . . . . 8
⊢ (ℎ = (Hom
‘(SetCat‘2o)) → (∃𝑧 ∈ 𝑏 ∃𝑤 ∈ 𝑏 (((𝑥ℎ𝑦) ∩ (𝑧ℎ𝑤)) ≠ ∅ ∧ ¬ (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ ∃𝑧 ∈ 𝑏 ∃𝑤 ∈ 𝑏 (((𝑥(Hom
‘(SetCat‘2o))𝑦) ∩ (𝑧(Hom
‘(SetCat‘2o))𝑤)) ≠ ∅ ∧ ¬ (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))) |
32 | 31 | 2rexbidv 3211 |
. . . . . . 7
⊢ (ℎ = (Hom
‘(SetCat‘2o)) → (∃𝑥 ∈ 𝑏 ∃𝑦 ∈ 𝑏 ∃𝑧 ∈ 𝑏 ∃𝑤 ∈ 𝑏 (((𝑥ℎ𝑦) ∩ (𝑧ℎ𝑤)) ≠ ∅ ∧ ¬ (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ ∃𝑥 ∈ 𝑏 ∃𝑦 ∈ 𝑏 ∃𝑧 ∈ 𝑏 ∃𝑤 ∈ 𝑏 (((𝑥(Hom
‘(SetCat‘2o))𝑦) ∩ (𝑧(Hom
‘(SetCat‘2o))𝑤)) ≠ ∅ ∧ ¬ (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))) |
33 | 32 | adantl 485 |
. . . . . 6
⊢ (((𝑐 = (SetCat‘2o)
∧ 𝑏 =
(Base‘(SetCat‘2o))) ∧ ℎ = (Hom ‘(SetCat‘2o)))
→ (∃𝑥 ∈
𝑏 ∃𝑦 ∈ 𝑏 ∃𝑧 ∈ 𝑏 ∃𝑤 ∈ 𝑏 (((𝑥ℎ𝑦) ∩ (𝑧ℎ𝑤)) ≠ ∅ ∧ ¬ (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ ∃𝑥 ∈ 𝑏 ∃𝑦 ∈ 𝑏 ∃𝑧 ∈ 𝑏 ∃𝑤 ∈ 𝑏 (((𝑥(Hom
‘(SetCat‘2o))𝑦) ∩ (𝑧(Hom
‘(SetCat‘2o))𝑤)) ≠ ∅ ∧ ¬ (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))) |
34 | | pm4.61 408 |
. . . . . . . . . . 11
⊢ (¬
(((𝑥ℎ𝑦) ∩ (𝑧ℎ𝑤)) ≠ ∅ → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ (((𝑥ℎ𝑦) ∩ (𝑧ℎ𝑤)) ≠ ∅ ∧ ¬ (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))) |
35 | 34 | 2rexbii 3163 |
. . . . . . . . . 10
⊢
(∃𝑧 ∈
𝑏 ∃𝑤 ∈ 𝑏 ¬ (((𝑥ℎ𝑦) ∩ (𝑧ℎ𝑤)) ≠ ∅ → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ ∃𝑧 ∈ 𝑏 ∃𝑤 ∈ 𝑏 (((𝑥ℎ𝑦) ∩ (𝑧ℎ𝑤)) ≠ ∅ ∧ ¬ (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))) |
36 | | rexnal2 3171 |
. . . . . . . . . 10
⊢
(∃𝑧 ∈
𝑏 ∃𝑤 ∈ 𝑏 ¬ (((𝑥ℎ𝑦) ∩ (𝑧ℎ𝑤)) ≠ ∅ → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ ¬ ∀𝑧 ∈ 𝑏 ∀𝑤 ∈ 𝑏 (((𝑥ℎ𝑦) ∩ (𝑧ℎ𝑤)) ≠ ∅ → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))) |
37 | 35, 36 | bitr3i 280 |
. . . . . . . . 9
⊢
(∃𝑧 ∈
𝑏 ∃𝑤 ∈ 𝑏 (((𝑥ℎ𝑦) ∩ (𝑧ℎ𝑤)) ≠ ∅ ∧ ¬ (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ ¬ ∀𝑧 ∈ 𝑏 ∀𝑤 ∈ 𝑏 (((𝑥ℎ𝑦) ∩ (𝑧ℎ𝑤)) ≠ ∅ → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))) |
38 | 37 | 2rexbii 3163 |
. . . . . . . 8
⊢
(∃𝑥 ∈
𝑏 ∃𝑦 ∈ 𝑏 ∃𝑧 ∈ 𝑏 ∃𝑤 ∈ 𝑏 (((𝑥ℎ𝑦) ∩ (𝑧ℎ𝑤)) ≠ ∅ ∧ ¬ (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ ∃𝑥 ∈ 𝑏 ∃𝑦 ∈ 𝑏 ¬ ∀𝑧 ∈ 𝑏 ∀𝑤 ∈ 𝑏 (((𝑥ℎ𝑦) ∩ (𝑧ℎ𝑤)) ≠ ∅ → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))) |
39 | | rexnal2 3171 |
. . . . . . . 8
⊢
(∃𝑥 ∈
𝑏 ∃𝑦 ∈ 𝑏 ¬ ∀𝑧 ∈ 𝑏 ∀𝑤 ∈ 𝑏 (((𝑥ℎ𝑦) ∩ (𝑧ℎ𝑤)) ≠ ∅ → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ ¬ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ∀𝑤 ∈ 𝑏 (((𝑥ℎ𝑦) ∩ (𝑧ℎ𝑤)) ≠ ∅ → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))) |
40 | 38, 39 | bitri 278 |
. . . . . . 7
⊢
(∃𝑥 ∈
𝑏 ∃𝑦 ∈ 𝑏 ∃𝑧 ∈ 𝑏 ∃𝑤 ∈ 𝑏 (((𝑥ℎ𝑦) ∩ (𝑧ℎ𝑤)) ≠ ∅ ∧ ¬ (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ ¬ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ∀𝑤 ∈ 𝑏 (((𝑥ℎ𝑦) ∩ (𝑧ℎ𝑤)) ≠ ∅ → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))) |
41 | 40 | a1i 11 |
. . . . . 6
⊢ (((𝑐 = (SetCat‘2o)
∧ 𝑏 =
(Base‘(SetCat‘2o))) ∧ ℎ = (Hom ‘(SetCat‘2o)))
→ (∃𝑥 ∈
𝑏 ∃𝑦 ∈ 𝑏 ∃𝑧 ∈ 𝑏 ∃𝑤 ∈ 𝑏 (((𝑥ℎ𝑦) ∩ (𝑧ℎ𝑤)) ≠ ∅ ∧ ¬ (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ ¬ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ∀𝑤 ∈ 𝑏 (((𝑥ℎ𝑦) ∩ (𝑧ℎ𝑤)) ≠ ∅ → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))) |
42 | | rexeq 3312 |
. . . . . . . . . 10
⊢ (𝑏 =
(Base‘(SetCat‘2o)) → (∃𝑤 ∈ 𝑏 (((𝑥(Hom
‘(SetCat‘2o))𝑦) ∩ (𝑧(Hom
‘(SetCat‘2o))𝑤)) ≠ ∅ ∧ ¬ (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ ∃𝑤 ∈
(Base‘(SetCat‘2o))(((𝑥(Hom
‘(SetCat‘2o))𝑦) ∩ (𝑧(Hom
‘(SetCat‘2o))𝑤)) ≠ ∅ ∧ ¬ (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))) |
43 | 42 | 2rexbidv 3211 |
. . . . . . . . 9
⊢ (𝑏 =
(Base‘(SetCat‘2o)) → (∃𝑦 ∈ 𝑏 ∃𝑧 ∈ 𝑏 ∃𝑤 ∈ 𝑏 (((𝑥(Hom
‘(SetCat‘2o))𝑦) ∩ (𝑧(Hom
‘(SetCat‘2o))𝑤)) ≠ ∅ ∧ ¬ (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ ∃𝑦 ∈ 𝑏 ∃𝑧 ∈ 𝑏 ∃𝑤 ∈
(Base‘(SetCat‘2o))(((𝑥(Hom
‘(SetCat‘2o))𝑦) ∩ (𝑧(Hom
‘(SetCat‘2o))𝑤)) ≠ ∅ ∧ ¬ (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))) |
44 | 43 | rexbidv 3208 |
. . . . . . . 8
⊢ (𝑏 =
(Base‘(SetCat‘2o)) → (∃𝑥 ∈ 𝑏 ∃𝑦 ∈ 𝑏 ∃𝑧 ∈ 𝑏 ∃𝑤 ∈ 𝑏 (((𝑥(Hom
‘(SetCat‘2o))𝑦) ∩ (𝑧(Hom
‘(SetCat‘2o))𝑤)) ≠ ∅ ∧ ¬ (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ ∃𝑥 ∈ 𝑏 ∃𝑦 ∈ 𝑏 ∃𝑧 ∈ 𝑏 ∃𝑤 ∈
(Base‘(SetCat‘2o))(((𝑥(Hom
‘(SetCat‘2o))𝑦) ∩ (𝑧(Hom
‘(SetCat‘2o))𝑤)) ≠ ∅ ∧ ¬ (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))) |
45 | | rexeq 3312 |
. . . . . . . . 9
⊢ (𝑏 =
(Base‘(SetCat‘2o)) → (∃𝑧 ∈ 𝑏 ∃𝑤 ∈
(Base‘(SetCat‘2o))(((𝑥(Hom
‘(SetCat‘2o))𝑦) ∩ (𝑧(Hom
‘(SetCat‘2o))𝑤)) ≠ ∅ ∧ ¬ (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ ∃𝑧 ∈
(Base‘(SetCat‘2o))∃𝑤 ∈
(Base‘(SetCat‘2o))(((𝑥(Hom
‘(SetCat‘2o))𝑦) ∩ (𝑧(Hom
‘(SetCat‘2o))𝑤)) ≠ ∅ ∧ ¬ (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))) |
46 | 45 | 2rexbidv 3211 |
. . . . . . . 8
⊢ (𝑏 =
(Base‘(SetCat‘2o)) → (∃𝑥 ∈ 𝑏 ∃𝑦 ∈ 𝑏 ∃𝑧 ∈ 𝑏 ∃𝑤 ∈
(Base‘(SetCat‘2o))(((𝑥(Hom
‘(SetCat‘2o))𝑦) ∩ (𝑧(Hom
‘(SetCat‘2o))𝑤)) ≠ ∅ ∧ ¬ (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ ∃𝑥 ∈ 𝑏 ∃𝑦 ∈ 𝑏 ∃𝑧 ∈
(Base‘(SetCat‘2o))∃𝑤 ∈
(Base‘(SetCat‘2o))(((𝑥(Hom
‘(SetCat‘2o))𝑦) ∩ (𝑧(Hom
‘(SetCat‘2o))𝑤)) ≠ ∅ ∧ ¬ (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))) |
47 | | rexeq 3312 |
. . . . . . . . 9
⊢ (𝑏 =
(Base‘(SetCat‘2o)) → (∃𝑦 ∈ 𝑏 ∃𝑧 ∈
(Base‘(SetCat‘2o))∃𝑤 ∈
(Base‘(SetCat‘2o))(((𝑥(Hom
‘(SetCat‘2o))𝑦) ∩ (𝑧(Hom
‘(SetCat‘2o))𝑤)) ≠ ∅ ∧ ¬ (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ ∃𝑦 ∈
(Base‘(SetCat‘2o))∃𝑧 ∈
(Base‘(SetCat‘2o))∃𝑤 ∈
(Base‘(SetCat‘2o))(((𝑥(Hom
‘(SetCat‘2o))𝑦) ∩ (𝑧(Hom
‘(SetCat‘2o))𝑤)) ≠ ∅ ∧ ¬ (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))) |
48 | 47 | rexeqbi1dv 3310 |
. . . . . . . 8
⊢ (𝑏 =
(Base‘(SetCat‘2o)) → (∃𝑥 ∈ 𝑏 ∃𝑦 ∈ 𝑏 ∃𝑧 ∈
(Base‘(SetCat‘2o))∃𝑤 ∈
(Base‘(SetCat‘2o))(((𝑥(Hom
‘(SetCat‘2o))𝑦) ∩ (𝑧(Hom
‘(SetCat‘2o))𝑤)) ≠ ∅ ∧ ¬ (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ ∃𝑥 ∈
(Base‘(SetCat‘2o))∃𝑦 ∈
(Base‘(SetCat‘2o))∃𝑧 ∈
(Base‘(SetCat‘2o))∃𝑤 ∈
(Base‘(SetCat‘2o))(((𝑥(Hom
‘(SetCat‘2o))𝑦) ∩ (𝑧(Hom
‘(SetCat‘2o))𝑤)) ≠ ∅ ∧ ¬ (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))) |
49 | 44, 46, 48 | 3bitrd 308 |
. . . . . . 7
⊢ (𝑏 =
(Base‘(SetCat‘2o)) → (∃𝑥 ∈ 𝑏 ∃𝑦 ∈ 𝑏 ∃𝑧 ∈ 𝑏 ∃𝑤 ∈ 𝑏 (((𝑥(Hom
‘(SetCat‘2o))𝑦) ∩ (𝑧(Hom
‘(SetCat‘2o))𝑤)) ≠ ∅ ∧ ¬ (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ ∃𝑥 ∈
(Base‘(SetCat‘2o))∃𝑦 ∈
(Base‘(SetCat‘2o))∃𝑧 ∈
(Base‘(SetCat‘2o))∃𝑤 ∈
(Base‘(SetCat‘2o))(((𝑥(Hom
‘(SetCat‘2o))𝑦) ∩ (𝑧(Hom
‘(SetCat‘2o))𝑤)) ≠ ∅ ∧ ¬ (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))) |
50 | 49 | ad2antlr 727 |
. . . . . 6
⊢ (((𝑐 = (SetCat‘2o)
∧ 𝑏 =
(Base‘(SetCat‘2o))) ∧ ℎ = (Hom ‘(SetCat‘2o)))
→ (∃𝑥 ∈
𝑏 ∃𝑦 ∈ 𝑏 ∃𝑧 ∈ 𝑏 ∃𝑤 ∈ 𝑏 (((𝑥(Hom
‘(SetCat‘2o))𝑦) ∩ (𝑧(Hom
‘(SetCat‘2o))𝑤)) ≠ ∅ ∧ ¬ (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ ∃𝑥 ∈
(Base‘(SetCat‘2o))∃𝑦 ∈
(Base‘(SetCat‘2o))∃𝑧 ∈
(Base‘(SetCat‘2o))∃𝑤 ∈
(Base‘(SetCat‘2o))(((𝑥(Hom
‘(SetCat‘2o))𝑦) ∩ (𝑧(Hom
‘(SetCat‘2o))𝑤)) ≠ ∅ ∧ ¬ (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))) |
51 | 33, 41, 50 | 3bitr3d 312 |
. . . . 5
⊢ (((𝑐 = (SetCat‘2o)
∧ 𝑏 =
(Base‘(SetCat‘2o))) ∧ ℎ = (Hom ‘(SetCat‘2o)))
→ (¬ ∀𝑥
∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ∀𝑤 ∈ 𝑏 (((𝑥ℎ𝑦) ∩ (𝑧ℎ𝑤)) ≠ ∅ → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ ∃𝑥 ∈
(Base‘(SetCat‘2o))∃𝑦 ∈
(Base‘(SetCat‘2o))∃𝑧 ∈
(Base‘(SetCat‘2o))∃𝑤 ∈
(Base‘(SetCat‘2o))(((𝑥(Hom
‘(SetCat‘2o))𝑦) ∩ (𝑧(Hom
‘(SetCat‘2o))𝑤)) ≠ ∅ ∧ ¬ (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))) |
52 | 23, 25, 51 | sbcied2 3732 |
. . . 4
⊢ ((𝑐 = (SetCat‘2o)
∧ 𝑏 =
(Base‘(SetCat‘2o))) → ([(Hom ‘𝑐) / ℎ] ¬ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ∀𝑤 ∈ 𝑏 (((𝑥ℎ𝑦) ∩ (𝑧ℎ𝑤)) ≠ ∅ → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ ∃𝑥 ∈
(Base‘(SetCat‘2o))∃𝑦 ∈
(Base‘(SetCat‘2o))∃𝑧 ∈
(Base‘(SetCat‘2o))∃𝑤 ∈
(Base‘(SetCat‘2o))(((𝑥(Hom
‘(SetCat‘2o))𝑦) ∩ (𝑧(Hom
‘(SetCat‘2o))𝑤)) ≠ ∅ ∧ ¬ (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))) |
53 | 21, 22, 52 | sbcied2 3732 |
. . 3
⊢ (𝑐 = (SetCat‘2o)
→ ([(Base‘𝑐) / 𝑏][(Hom ‘𝑐) / ℎ] ¬ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ∀𝑤 ∈ 𝑏 (((𝑥ℎ𝑦) ∩ (𝑧ℎ𝑤)) ≠ ∅ → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ ∃𝑥 ∈
(Base‘(SetCat‘2o))∃𝑦 ∈
(Base‘(SetCat‘2o))∃𝑧 ∈
(Base‘(SetCat‘2o))∃𝑤 ∈
(Base‘(SetCat‘2o))(((𝑥(Hom
‘(SetCat‘2o))𝑦) ∩ (𝑧(Hom
‘(SetCat‘2o))𝑤)) ≠ ∅ ∧ ¬ (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))) |
54 | 53 | rspcev 3529 |
. 2
⊢
(((SetCat‘2o) ∈ Cat ∧ ∃𝑥 ∈
(Base‘(SetCat‘2o))∃𝑦 ∈
(Base‘(SetCat‘2o))∃𝑧 ∈
(Base‘(SetCat‘2o))∃𝑤 ∈
(Base‘(SetCat‘2o))(((𝑥(Hom
‘(SetCat‘2o))𝑦) ∩ (𝑧(Hom
‘(SetCat‘2o))𝑤)) ≠ ∅ ∧ ¬ (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))) → ∃𝑐 ∈ Cat [(Base‘𝑐) / 𝑏][(Hom ‘𝑐) / ℎ] ¬ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ∀𝑤 ∈ 𝑏 (((𝑥ℎ𝑦) ∩ (𝑧ℎ𝑤)) ≠ ∅ → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))) |
55 | 4, 20, 54 | mp2an 692 |
1
⊢
∃𝑐 ∈ Cat
[(Base‘𝑐) /
𝑏][(Hom
‘𝑐) / ℎ] ¬ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ∀𝑤 ∈ 𝑏 (((𝑥ℎ𝑦) ∩ (𝑧ℎ𝑤)) ≠ ∅ → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) |