Proof of Theorem cat1
| Step | Hyp | Ref
| Expression |
| 1 | | 2on 8520 |
. . 3
⊢
2o ∈ On |
| 2 | | eqid 2737 |
. . . 4
⊢
(SetCat‘2o) =
(SetCat‘2o) |
| 3 | 2 | setccat 18130 |
. . 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 2737 |
. . . 4
⊢
(Base‘(SetCat‘2o)) =
(Base‘(SetCat‘2o)) |
| 7 | | eqid 2737 |
. . . 4
⊢ (Hom
‘(SetCat‘2o)) = (Hom
‘(SetCat‘2o)) |
| 8 | | 0ex 5307 |
. . . . . . 7
⊢ ∅
∈ V |
| 9 | 8 | prid1 4762 |
. . . . . 6
⊢ ∅
∈ {∅, {∅}} |
| 10 | | df2o2 8515 |
. . . . . 6
⊢
2o = {∅, {∅}} |
| 11 | 9, 10 | eleqtrri 2840 |
. . . . 5
⊢ ∅
∈ 2o |
| 12 | 11 | a1i 11 |
. . . 4
⊢ (⊤
→ ∅ ∈ 2o) |
| 13 | | p0ex 5384 |
. . . . . . 7
⊢ {∅}
∈ V |
| 14 | 13 | prid2 4763 |
. . . . . 6
⊢ {∅}
∈ {∅, {∅}} |
| 15 | 14, 10 | eleqtrri 2840 |
. . . . 5
⊢ {∅}
∈ 2o |
| 16 | 15 | a1i 11 |
. . . 4
⊢ (⊤
→ {∅} ∈ 2o) |
| 17 | | 0nep0 5358 |
. . . . 5
⊢ ∅
≠ {∅} |
| 18 | 17 | a1i 11 |
. . . 4
⊢ (⊤
→ ∅ ≠ {∅}) |
| 19 | 2, 5, 6, 7, 12, 16, 18 | cat1lem 18141 |
. . 3
⊢ (⊤
→ ∃𝑥 ∈
(Base‘(SetCat‘2o))∃𝑦 ∈
(Base‘(SetCat‘2o))∃𝑧 ∈
(Base‘(SetCat‘2o))∃𝑤 ∈
(Base‘(SetCat‘2o))(((𝑥(Hom
‘(SetCat‘2o))𝑦) ∩ (𝑧(Hom
‘(SetCat‘2o))𝑤)) ≠ ∅ ∧ ¬ (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))) |
| 20 | 19 | mptru 1547 |
. 2
⊢
∃𝑥 ∈
(Base‘(SetCat‘2o))∃𝑦 ∈
(Base‘(SetCat‘2o))∃𝑧 ∈
(Base‘(SetCat‘2o))∃𝑤 ∈
(Base‘(SetCat‘2o))(((𝑥(Hom
‘(SetCat‘2o))𝑦) ∩ (𝑧(Hom
‘(SetCat‘2o))𝑤)) ≠ ∅ ∧ ¬ (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) |
| 21 | | fvexd 6921 |
. . . 4
⊢ (𝑐 = (SetCat‘2o)
→ (Base‘𝑐)
∈ V) |
| 22 | | fveq2 6906 |
. . . 4
⊢ (𝑐 = (SetCat‘2o)
→ (Base‘𝑐) =
(Base‘(SetCat‘2o))) |
| 23 | | fvexd 6921 |
. . . . 5
⊢ ((𝑐 = (SetCat‘2o)
∧ 𝑏 =
(Base‘(SetCat‘2o))) → (Hom ‘𝑐) ∈ V) |
| 24 | | fveq2 6906 |
. . . . . 6
⊢ (𝑐 = (SetCat‘2o)
→ (Hom ‘𝑐) =
(Hom ‘(SetCat‘2o))) |
| 25 | 24 | adantr 480 |
. . . . 5
⊢ ((𝑐 = (SetCat‘2o)
∧ 𝑏 =
(Base‘(SetCat‘2o))) → (Hom ‘𝑐) = (Hom
‘(SetCat‘2o))) |
| 26 | | oveq 7437 |
. . . . . . . . . . . 12
⊢ (ℎ = (Hom
‘(SetCat‘2o)) → (𝑥ℎ𝑦) = (𝑥(Hom
‘(SetCat‘2o))𝑦)) |
| 27 | | oveq 7437 |
. . . . . . . . . . . 12
⊢ (ℎ = (Hom
‘(SetCat‘2o)) → (𝑧ℎ𝑤) = (𝑧(Hom
‘(SetCat‘2o))𝑤)) |
| 28 | 26, 27 | ineq12d 4221 |
. . . . . . . . . . 11
⊢ (ℎ = (Hom
‘(SetCat‘2o)) → ((𝑥ℎ𝑦) ∩ (𝑧ℎ𝑤)) = ((𝑥(Hom
‘(SetCat‘2o))𝑦) ∩ (𝑧(Hom
‘(SetCat‘2o))𝑤))) |
| 29 | 28 | neeq1d 3000 |
. . . . . . . . . 10
⊢ (ℎ = (Hom
‘(SetCat‘2o)) → (((𝑥ℎ𝑦) ∩ (𝑧ℎ𝑤)) ≠ ∅ ↔ ((𝑥(Hom
‘(SetCat‘2o))𝑦) ∩ (𝑧(Hom
‘(SetCat‘2o))𝑤)) ≠ ∅)) |
| 30 | 29 | anbi1d 631 |
. . . . . . . . 9
⊢ (ℎ = (Hom
‘(SetCat‘2o)) → ((((𝑥ℎ𝑦) ∩ (𝑧ℎ𝑤)) ≠ ∅ ∧ ¬ (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ (((𝑥(Hom
‘(SetCat‘2o))𝑦) ∩ (𝑧(Hom
‘(SetCat‘2o))𝑤)) ≠ ∅ ∧ ¬ (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))) |
| 31 | 30 | 2rexbidv 3222 |
. . . . . . . 8
⊢ (ℎ = (Hom
‘(SetCat‘2o)) → (∃𝑧 ∈ 𝑏 ∃𝑤 ∈ 𝑏 (((𝑥ℎ𝑦) ∩ (𝑧ℎ𝑤)) ≠ ∅ ∧ ¬ (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ ∃𝑧 ∈ 𝑏 ∃𝑤 ∈ 𝑏 (((𝑥(Hom
‘(SetCat‘2o))𝑦) ∩ (𝑧(Hom
‘(SetCat‘2o))𝑤)) ≠ ∅ ∧ ¬ (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))) |
| 32 | 31 | 2rexbidv 3222 |
. . . . . . 7
⊢ (ℎ = (Hom
‘(SetCat‘2o)) → (∃𝑥 ∈ 𝑏 ∃𝑦 ∈ 𝑏 ∃𝑧 ∈ 𝑏 ∃𝑤 ∈ 𝑏 (((𝑥ℎ𝑦) ∩ (𝑧ℎ𝑤)) ≠ ∅ ∧ ¬ (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ ∃𝑥 ∈ 𝑏 ∃𝑦 ∈ 𝑏 ∃𝑧 ∈ 𝑏 ∃𝑤 ∈ 𝑏 (((𝑥(Hom
‘(SetCat‘2o))𝑦) ∩ (𝑧(Hom
‘(SetCat‘2o))𝑤)) ≠ ∅ ∧ ¬ (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))) |
| 33 | 32 | adantl 481 |
. . . . . 6
⊢ (((𝑐 = (SetCat‘2o)
∧ 𝑏 =
(Base‘(SetCat‘2o))) ∧ ℎ = (Hom ‘(SetCat‘2o)))
→ (∃𝑥 ∈
𝑏 ∃𝑦 ∈ 𝑏 ∃𝑧 ∈ 𝑏 ∃𝑤 ∈ 𝑏 (((𝑥ℎ𝑦) ∩ (𝑧ℎ𝑤)) ≠ ∅ ∧ ¬ (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ ∃𝑥 ∈ 𝑏 ∃𝑦 ∈ 𝑏 ∃𝑧 ∈ 𝑏 ∃𝑤 ∈ 𝑏 (((𝑥(Hom
‘(SetCat‘2o))𝑦) ∩ (𝑧(Hom
‘(SetCat‘2o))𝑤)) ≠ ∅ ∧ ¬ (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))) |
| 34 | | pm4.61 404 |
. . . . . . . . . . 11
⊢ (¬
(((𝑥ℎ𝑦) ∩ (𝑧ℎ𝑤)) ≠ ∅ → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ (((𝑥ℎ𝑦) ∩ (𝑧ℎ𝑤)) ≠ ∅ ∧ ¬ (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))) |
| 35 | 34 | 2rexbii 3129 |
. . . . . . . . . 10
⊢
(∃𝑧 ∈
𝑏 ∃𝑤 ∈ 𝑏 ¬ (((𝑥ℎ𝑦) ∩ (𝑧ℎ𝑤)) ≠ ∅ → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ ∃𝑧 ∈ 𝑏 ∃𝑤 ∈ 𝑏 (((𝑥ℎ𝑦) ∩ (𝑧ℎ𝑤)) ≠ ∅ ∧ ¬ (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))) |
| 36 | | rexnal2 3135 |
. . . . . . . . . 10
⊢
(∃𝑧 ∈
𝑏 ∃𝑤 ∈ 𝑏 ¬ (((𝑥ℎ𝑦) ∩ (𝑧ℎ𝑤)) ≠ ∅ → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ ¬ ∀𝑧 ∈ 𝑏 ∀𝑤 ∈ 𝑏 (((𝑥ℎ𝑦) ∩ (𝑧ℎ𝑤)) ≠ ∅ → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))) |
| 37 | 35, 36 | bitr3i 277 |
. . . . . . . . 9
⊢
(∃𝑧 ∈
𝑏 ∃𝑤 ∈ 𝑏 (((𝑥ℎ𝑦) ∩ (𝑧ℎ𝑤)) ≠ ∅ ∧ ¬ (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ ¬ ∀𝑧 ∈ 𝑏 ∀𝑤 ∈ 𝑏 (((𝑥ℎ𝑦) ∩ (𝑧ℎ𝑤)) ≠ ∅ → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))) |
| 38 | 37 | 2rexbii 3129 |
. . . . . . . 8
⊢
(∃𝑥 ∈
𝑏 ∃𝑦 ∈ 𝑏 ∃𝑧 ∈ 𝑏 ∃𝑤 ∈ 𝑏 (((𝑥ℎ𝑦) ∩ (𝑧ℎ𝑤)) ≠ ∅ ∧ ¬ (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ ∃𝑥 ∈ 𝑏 ∃𝑦 ∈ 𝑏 ¬ ∀𝑧 ∈ 𝑏 ∀𝑤 ∈ 𝑏 (((𝑥ℎ𝑦) ∩ (𝑧ℎ𝑤)) ≠ ∅ → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))) |
| 39 | | rexnal2 3135 |
. . . . . . . 8
⊢
(∃𝑥 ∈
𝑏 ∃𝑦 ∈ 𝑏 ¬ ∀𝑧 ∈ 𝑏 ∀𝑤 ∈ 𝑏 (((𝑥ℎ𝑦) ∩ (𝑧ℎ𝑤)) ≠ ∅ → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ ¬ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ∀𝑤 ∈ 𝑏 (((𝑥ℎ𝑦) ∩ (𝑧ℎ𝑤)) ≠ ∅ → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))) |
| 40 | 38, 39 | bitri 275 |
. . . . . . 7
⊢
(∃𝑥 ∈
𝑏 ∃𝑦 ∈ 𝑏 ∃𝑧 ∈ 𝑏 ∃𝑤 ∈ 𝑏 (((𝑥ℎ𝑦) ∩ (𝑧ℎ𝑤)) ≠ ∅ ∧ ¬ (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ ¬ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ∀𝑤 ∈ 𝑏 (((𝑥ℎ𝑦) ∩ (𝑧ℎ𝑤)) ≠ ∅ → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))) |
| 41 | 40 | a1i 11 |
. . . . . 6
⊢ (((𝑐 = (SetCat‘2o)
∧ 𝑏 =
(Base‘(SetCat‘2o))) ∧ ℎ = (Hom ‘(SetCat‘2o)))
→ (∃𝑥 ∈
𝑏 ∃𝑦 ∈ 𝑏 ∃𝑧 ∈ 𝑏 ∃𝑤 ∈ 𝑏 (((𝑥ℎ𝑦) ∩ (𝑧ℎ𝑤)) ≠ ∅ ∧ ¬ (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ ¬ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ∀𝑤 ∈ 𝑏 (((𝑥ℎ𝑦) ∩ (𝑧ℎ𝑤)) ≠ ∅ → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))) |
| 42 | | rexeq 3322 |
. . . . . . . . . 10
⊢ (𝑏 =
(Base‘(SetCat‘2o)) → (∃𝑤 ∈ 𝑏 (((𝑥(Hom
‘(SetCat‘2o))𝑦) ∩ (𝑧(Hom
‘(SetCat‘2o))𝑤)) ≠ ∅ ∧ ¬ (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ ∃𝑤 ∈
(Base‘(SetCat‘2o))(((𝑥(Hom
‘(SetCat‘2o))𝑦) ∩ (𝑧(Hom
‘(SetCat‘2o))𝑤)) ≠ ∅ ∧ ¬ (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))) |
| 43 | 42 | 2rexbidv 3222 |
. . . . . . . . 9
⊢ (𝑏 =
(Base‘(SetCat‘2o)) → (∃𝑦 ∈ 𝑏 ∃𝑧 ∈ 𝑏 ∃𝑤 ∈ 𝑏 (((𝑥(Hom
‘(SetCat‘2o))𝑦) ∩ (𝑧(Hom
‘(SetCat‘2o))𝑤)) ≠ ∅ ∧ ¬ (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ ∃𝑦 ∈ 𝑏 ∃𝑧 ∈ 𝑏 ∃𝑤 ∈
(Base‘(SetCat‘2o))(((𝑥(Hom
‘(SetCat‘2o))𝑦) ∩ (𝑧(Hom
‘(SetCat‘2o))𝑤)) ≠ ∅ ∧ ¬ (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))) |
| 44 | 43 | rexbidv 3179 |
. . . . . . . 8
⊢ (𝑏 =
(Base‘(SetCat‘2o)) → (∃𝑥 ∈ 𝑏 ∃𝑦 ∈ 𝑏 ∃𝑧 ∈ 𝑏 ∃𝑤 ∈ 𝑏 (((𝑥(Hom
‘(SetCat‘2o))𝑦) ∩ (𝑧(Hom
‘(SetCat‘2o))𝑤)) ≠ ∅ ∧ ¬ (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ ∃𝑥 ∈ 𝑏 ∃𝑦 ∈ 𝑏 ∃𝑧 ∈ 𝑏 ∃𝑤 ∈
(Base‘(SetCat‘2o))(((𝑥(Hom
‘(SetCat‘2o))𝑦) ∩ (𝑧(Hom
‘(SetCat‘2o))𝑤)) ≠ ∅ ∧ ¬ (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)))) |
| 45 | | rexeq 3322 |
. . . . . . . . 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 3222 |
. . . . . . . 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 3322 |
. . . . . . . . 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 3339 |
. . . . . . . 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 305 |
. . . . . . 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 309 |
. . . . 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 3833 |
. . . 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 3833 |
. . 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 3622 |
. 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
‘𝑐) / ℎ] ¬ ∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ∀𝑤 ∈ 𝑏 (((𝑥ℎ𝑦) ∩ (𝑧ℎ𝑤)) ≠ ∅ → (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) |