Proof of Theorem cat1lem
Step | Hyp | Ref
| Expression |
1 | | cat1lem.5 |
. . 3
⊢ (𝜑 → ∅ ∈ 𝑈) |
2 | | cat1lem.1 |
. . . . 5
⊢ 𝐶 = (SetCat‘𝑈) |
3 | | cat1lem.2 |
. . . . 5
⊢ (𝜑 → 𝑈 ∈ 𝑉) |
4 | 2, 3 | setcbas 17793 |
. . . 4
⊢ (𝜑 → 𝑈 = (Base‘𝐶)) |
5 | | cat1lem.3 |
. . . 4
⊢ 𝐵 = (Base‘𝐶) |
6 | 4, 5 | eqtr4di 2796 |
. . 3
⊢ (𝜑 → 𝑈 = 𝐵) |
7 | 1, 6 | eleqtrd 2841 |
. 2
⊢ (𝜑 → ∅ ∈ 𝐵) |
8 | | cat1lem.6 |
. . . 4
⊢ (𝜑 → 𝑌 ∈ 𝑈) |
9 | 8, 6 | eleqtrd 2841 |
. . 3
⊢ (𝜑 → 𝑌 ∈ 𝐵) |
10 | | f0 6655 |
. . . . 5
⊢
∅:∅⟶∅ |
11 | | cat1lem.4 |
. . . . . 6
⊢ 𝐻 = (Hom ‘𝐶) |
12 | 2, 3, 11, 1, 1 | elsetchom 17796 |
. . . . 5
⊢ (𝜑 → (∅ ∈
(∅𝐻∅) ↔
∅:∅⟶∅)) |
13 | 10, 12 | mpbiri 257 |
. . . 4
⊢ (𝜑 → ∅ ∈
(∅𝐻∅)) |
14 | | f0 6655 |
. . . . 5
⊢
∅:∅⟶𝑌 |
15 | 2, 3, 11, 1, 8 | elsetchom 17796 |
. . . . 5
⊢ (𝜑 → (∅ ∈
(∅𝐻𝑌) ↔ ∅:∅⟶𝑌)) |
16 | 14, 15 | mpbiri 257 |
. . . 4
⊢ (𝜑 → ∅ ∈
(∅𝐻𝑌)) |
17 | | inelcm 4398 |
. . . 4
⊢ ((∅
∈ (∅𝐻∅)
∧ ∅ ∈ (∅𝐻𝑌)) → ((∅𝐻∅) ∩ (∅𝐻𝑌)) ≠ ∅) |
18 | 13, 16, 17 | syl2anc 584 |
. . 3
⊢ (𝜑 → ((∅𝐻∅) ∩ (∅𝐻𝑌)) ≠ ∅) |
19 | | cat1lem.7 |
. . . . 5
⊢ (𝜑 → ∅ ≠ 𝑌) |
20 | 19 | neneqd 2948 |
. . . 4
⊢ (𝜑 → ¬ ∅ = 𝑌) |
21 | 20 | intnand 489 |
. . 3
⊢ (𝜑 → ¬ (∅ = ∅
∧ ∅ = 𝑌)) |
22 | | oveq1 7282 |
. . . . . . 7
⊢ (𝑧 = ∅ → (𝑧𝐻𝑤) = (∅𝐻𝑤)) |
23 | 22 | ineq2d 4146 |
. . . . . 6
⊢ (𝑧 = ∅ → ((∅𝐻∅) ∩ (𝑧𝐻𝑤)) = ((∅𝐻∅) ∩ (∅𝐻𝑤))) |
24 | 23 | neeq1d 3003 |
. . . . 5
⊢ (𝑧 = ∅ →
(((∅𝐻∅) ∩
(𝑧𝐻𝑤)) ≠ ∅ ↔ ((∅𝐻∅) ∩ (∅𝐻𝑤)) ≠ ∅)) |
25 | | eqeq2 2750 |
. . . . . . 7
⊢ (𝑧 = ∅ → (∅ =
𝑧 ↔ ∅ =
∅)) |
26 | 25 | anbi1d 630 |
. . . . . 6
⊢ (𝑧 = ∅ → ((∅ =
𝑧 ∧ ∅ = 𝑤) ↔ (∅ = ∅
∧ ∅ = 𝑤))) |
27 | 26 | notbid 318 |
. . . . 5
⊢ (𝑧 = ∅ → (¬
(∅ = 𝑧 ∧ ∅
= 𝑤) ↔ ¬ (∅
= ∅ ∧ ∅ = 𝑤))) |
28 | 24, 27 | anbi12d 631 |
. . . 4
⊢ (𝑧 = ∅ →
((((∅𝐻∅) ∩
(𝑧𝐻𝑤)) ≠ ∅ ∧ ¬ (∅ = 𝑧 ∧ ∅ = 𝑤)) ↔ (((∅𝐻∅) ∩ (∅𝐻𝑤)) ≠ ∅ ∧ ¬ (∅ =
∅ ∧ ∅ = 𝑤)))) |
29 | | oveq2 7283 |
. . . . . . 7
⊢ (𝑤 = 𝑌 → (∅𝐻𝑤) = (∅𝐻𝑌)) |
30 | 29 | ineq2d 4146 |
. . . . . 6
⊢ (𝑤 = 𝑌 → ((∅𝐻∅) ∩ (∅𝐻𝑤)) = ((∅𝐻∅) ∩ (∅𝐻𝑌))) |
31 | 30 | neeq1d 3003 |
. . . . 5
⊢ (𝑤 = 𝑌 → (((∅𝐻∅) ∩ (∅𝐻𝑤)) ≠ ∅ ↔ ((∅𝐻∅) ∩ (∅𝐻𝑌)) ≠ ∅)) |
32 | | eqeq2 2750 |
. . . . . . 7
⊢ (𝑤 = 𝑌 → (∅ = 𝑤 ↔ ∅ = 𝑌)) |
33 | 32 | anbi2d 629 |
. . . . . 6
⊢ (𝑤 = 𝑌 → ((∅ = ∅ ∧ ∅ =
𝑤) ↔ (∅ =
∅ ∧ ∅ = 𝑌))) |
34 | 33 | notbid 318 |
. . . . 5
⊢ (𝑤 = 𝑌 → (¬ (∅ = ∅ ∧
∅ = 𝑤) ↔ ¬
(∅ = ∅ ∧ ∅ = 𝑌))) |
35 | 31, 34 | anbi12d 631 |
. . . 4
⊢ (𝑤 = 𝑌 → ((((∅𝐻∅) ∩ (∅𝐻𝑤)) ≠ ∅ ∧ ¬ (∅ =
∅ ∧ ∅ = 𝑤))
↔ (((∅𝐻∅)
∩ (∅𝐻𝑌)) ≠ ∅ ∧ ¬
(∅ = ∅ ∧ ∅ = 𝑌)))) |
36 | 28, 35 | rspc2ev 3572 |
. . 3
⊢ ((∅
∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ (((∅𝐻∅) ∩ (∅𝐻𝑌)) ≠ ∅ ∧ ¬ (∅ =
∅ ∧ ∅ = 𝑌))) → ∃𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐵 (((∅𝐻∅) ∩ (𝑧𝐻𝑤)) ≠ ∅ ∧ ¬ (∅ = 𝑧 ∧ ∅ = 𝑤))) |
37 | 7, 9, 18, 21, 36 | syl112anc 1373 |
. 2
⊢ (𝜑 → ∃𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐵 (((∅𝐻∅) ∩ (𝑧𝐻𝑤)) ≠ ∅ ∧ ¬ (∅ = 𝑧 ∧ ∅ = 𝑤))) |
38 | | oveq1 7282 |
. . . . . . 7
⊢ (𝑥 = ∅ → (𝑥𝐻𝑦) = (∅𝐻𝑦)) |
39 | 38 | ineq1d 4145 |
. . . . . 6
⊢ (𝑥 = ∅ → ((𝑥𝐻𝑦) ∩ (𝑧𝐻𝑤)) = ((∅𝐻𝑦) ∩ (𝑧𝐻𝑤))) |
40 | 39 | neeq1d 3003 |
. . . . 5
⊢ (𝑥 = ∅ → (((𝑥𝐻𝑦) ∩ (𝑧𝐻𝑤)) ≠ ∅ ↔ ((∅𝐻𝑦) ∩ (𝑧𝐻𝑤)) ≠ ∅)) |
41 | | eqeq1 2742 |
. . . . . . 7
⊢ (𝑥 = ∅ → (𝑥 = 𝑧 ↔ ∅ = 𝑧)) |
42 | 41 | anbi1d 630 |
. . . . . 6
⊢ (𝑥 = ∅ → ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) ↔ (∅ = 𝑧 ∧ 𝑦 = 𝑤))) |
43 | 42 | notbid 318 |
. . . . 5
⊢ (𝑥 = ∅ → (¬ (𝑥 = 𝑧 ∧ 𝑦 = 𝑤) ↔ ¬ (∅ = 𝑧 ∧ 𝑦 = 𝑤))) |
44 | 40, 43 | anbi12d 631 |
. . . 4
⊢ (𝑥 = ∅ → ((((𝑥𝐻𝑦) ∩ (𝑧𝐻𝑤)) ≠ ∅ ∧ ¬ (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ (((∅𝐻𝑦) ∩ (𝑧𝐻𝑤)) ≠ ∅ ∧ ¬ (∅ = 𝑧 ∧ 𝑦 = 𝑤)))) |
45 | 44 | 2rexbidv 3229 |
. . 3
⊢ (𝑥 = ∅ → (∃𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐵 (((𝑥𝐻𝑦) ∩ (𝑧𝐻𝑤)) ≠ ∅ ∧ ¬ (𝑥 = 𝑧 ∧ 𝑦 = 𝑤)) ↔ ∃𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐵 (((∅𝐻𝑦) ∩ (𝑧𝐻𝑤)) ≠ ∅ ∧ ¬ (∅ = 𝑧 ∧ 𝑦 = 𝑤)))) |
46 | | oveq2 7283 |
. . . . . . 7
⊢ (𝑦 = ∅ → (∅𝐻𝑦) = (∅𝐻∅)) |
47 | 46 | ineq1d 4145 |
. . . . . 6
⊢ (𝑦 = ∅ → ((∅𝐻𝑦) ∩ (𝑧𝐻𝑤)) = ((∅𝐻∅) ∩ (𝑧𝐻𝑤))) |
48 | 47 | neeq1d 3003 |
. . . . 5
⊢ (𝑦 = ∅ →
(((∅𝐻𝑦) ∩ (𝑧𝐻𝑤)) ≠ ∅ ↔ ((∅𝐻∅) ∩ (𝑧𝐻𝑤)) ≠ ∅)) |
49 | | eqeq1 2742 |
. . . . . . 7
⊢ (𝑦 = ∅ → (𝑦 = 𝑤 ↔ ∅ = 𝑤)) |
50 | 49 | anbi2d 629 |
. . . . . 6
⊢ (𝑦 = ∅ → ((∅ =
𝑧 ∧ 𝑦 = 𝑤) ↔ (∅ = 𝑧 ∧ ∅ = 𝑤))) |
51 | 50 | notbid 318 |
. . . . 5
⊢ (𝑦 = ∅ → (¬
(∅ = 𝑧 ∧ 𝑦 = 𝑤) ↔ ¬ (∅ = 𝑧 ∧ ∅ = 𝑤))) |
52 | 48, 51 | anbi12d 631 |
. . . 4
⊢ (𝑦 = ∅ →
((((∅𝐻𝑦) ∩ (𝑧𝐻𝑤)) ≠ ∅ ∧ ¬ (∅ = 𝑧 ∧ 𝑦 = 𝑤)) ↔ (((∅𝐻∅) ∩ (𝑧𝐻𝑤)) ≠ ∅ ∧ ¬ (∅ = 𝑧 ∧ ∅ = 𝑤)))) |
53 | 52 | 2rexbidv 3229 |
. . 3
⊢ (𝑦 = ∅ → (∃𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐵 (((∅𝐻𝑦) ∩ (𝑧𝐻𝑤)) ≠ ∅ ∧ ¬ (∅ = 𝑧 ∧ 𝑦 = 𝑤)) ↔ ∃𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐵 (((∅𝐻∅) ∩ (𝑧𝐻𝑤)) ≠ ∅ ∧ ¬ (∅ = 𝑧 ∧ ∅ = 𝑤)))) |
54 | 45, 53 | rspc2ev 3572 |
. 2
⊢ ((∅
∈ 𝐵 ∧ ∅
∈ 𝐵 ∧ ∃𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐵 (((∅𝐻∅) ∩ (𝑧𝐻𝑤)) ≠ ∅ ∧ ¬ (∅ = 𝑧 ∧ ∅ = 𝑤))) → ∃𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐵 (((𝑥𝐻𝑦) ∩ (𝑧𝐻𝑤)) ≠ ∅ ∧ ¬ (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))) |
55 | 7, 7, 37, 54 | syl3anc 1370 |
1
⊢ (𝜑 → ∃𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐵 (((𝑥𝐻𝑦) ∩ (𝑧𝐻𝑤)) ≠ ∅ ∧ ¬ (𝑥 = 𝑧 ∧ 𝑦 = 𝑤))) |