Metamath Proof Explorer

Theorem cat1

Description: The definition of category df-cat does not impose pairwise disjoint hom-sets as required in Axiom CAT 1 in Lang p. 53. See setc2obas and setc2ohom for a counterexample. For a version with pairwise disjoint hom-sets, see df-homa and its subsection. (Contributed by Zhi Wang, 15-Sep-2024)

Ref Expression
Assertion cat1 ∃ 𝑐 ∈ Cat [ ( Base ‘ 𝑐 ) / 𝑏 ] [ ( Hom ‘ 𝑐 ) / ℎ ] ¬ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ∀ 𝑤 ∈ 𝑏 ( ( ( 𝑥 ℎ 𝑦 ) ∩ ( 𝑧 ℎ 𝑤 ) ) ≠ ∅ → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) )

Proof

Step Hyp Ref Expression
1 2on ⊢ 2o ∈ On
2 eqid ⊢ ( SetCat ‘ 2o ) = ( SetCat ‘ 2o )
3 2 setccat ⊢ ( 2o ∈ On → ( SetCat ‘ 2o ) ∈ Cat )
4 1 3 ax-mp ⊢ ( SetCat ‘ 2o ) ∈ Cat
5 1 a1i ⊢ ( ⊤ → 2o ∈ On )
6 eqid ⊢ ( Base ‘ ( SetCat ‘ 2o ) ) = ( Base ‘ ( SetCat ‘ 2o ) )
7 eqid ⊢ ( Hom ‘ ( SetCat ‘ 2o ) ) = ( Hom ‘ ( SetCat ‘ 2o ) )
8 0ex ⊢ ∅ ∈ V
9 8 prid1 ⊢ ∅ ∈ { ∅ , { ∅ } }
10 df2o2 ⊢ 2o = { ∅ , { ∅ } }
11 9 10 eleqtrri ⊢ ∅ ∈ 2o
12 11 a1i ⊢ ( ⊤ → ∅ ∈ 2o )
13 p0ex ⊢ { ∅ } ∈ V
14 13 prid2 ⊢ { ∅ } ∈ { ∅ , { ∅ } }
15 14 10 eleqtrri ⊢ { ∅ } ∈ 2o
16 15 a1i ⊢ ( ⊤ → { ∅ } ∈ 2o )
17 0nep0 ⊢ ∅ ≠ { ∅ }
18 17 a1i ⊢ ( ⊤ → ∅ ≠ { ∅ } )
19 2 5 6 7 12 16 18 cat1lem ⊢ ( ⊤ → ∃ 𝑥 ∈ ( Base ‘ ( SetCat ‘ 2o ) ) ∃ 𝑦 ∈ ( Base ‘ ( SetCat ‘ 2o ) ) ∃ 𝑧 ∈ ( Base ‘ ( SetCat ‘ 2o ) ) ∃ 𝑤 ∈ ( Base ‘ ( SetCat ‘ 2o ) ) ( ( ( 𝑥 ( Hom ‘ ( SetCat ‘ 2o ) ) 𝑦 ) ∩ ( 𝑧 ( Hom ‘ ( SetCat ‘ 2o ) ) 𝑤 ) ) ≠ ∅ ∧ ¬ ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) )
20 19 mptru ⊢ ∃ 𝑥 ∈ ( Base ‘ ( SetCat ‘ 2o ) ) ∃ 𝑦 ∈ ( Base ‘ ( SetCat ‘ 2o ) ) ∃ 𝑧 ∈ ( Base ‘ ( SetCat ‘ 2o ) ) ∃ 𝑤 ∈ ( Base ‘ ( SetCat ‘ 2o ) ) ( ( ( 𝑥 ( Hom ‘ ( SetCat ‘ 2o ) ) 𝑦 ) ∩ ( 𝑧 ( Hom ‘ ( SetCat ‘ 2o ) ) 𝑤 ) ) ≠ ∅ ∧ ¬ ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) )
21 fvexd ⊢ ( 𝑐 = ( SetCat ‘ 2o ) → ( Base ‘ 𝑐 ) ∈ V )
22 fveq2 ⊢ ( 𝑐 = ( SetCat ‘ 2o ) → ( Base ‘ 𝑐 ) = ( Base ‘ ( SetCat ‘ 2o ) ) )
23 fvexd ⊢ ( ( 𝑐 = ( SetCat ‘ 2o ) ∧ 𝑏 = ( Base ‘ ( SetCat ‘ 2o ) ) ) → ( Hom ‘ 𝑐 ) ∈ V )
24 fveq2 ⊢ ( 𝑐 = ( SetCat ‘ 2o ) → ( Hom ‘ 𝑐 ) = ( Hom ‘ ( SetCat ‘ 2o ) ) )
25 24 adantr ⊢ ( ( 𝑐 = ( SetCat ‘ 2o ) ∧ 𝑏 = ( Base ‘ ( SetCat ‘ 2o ) ) ) → ( Hom ‘ 𝑐 ) = ( Hom ‘ ( SetCat ‘ 2o ) ) )
26 oveq ⊢ ( ℎ = ( Hom ‘ ( SetCat ‘ 2o ) ) → ( 𝑥 ℎ 𝑦 ) = ( 𝑥 ( Hom ‘ ( SetCat ‘ 2o ) ) 𝑦 ) )
27 oveq ⊢ ( ℎ = ( Hom ‘ ( SetCat ‘ 2o ) ) → ( 𝑧 ℎ 𝑤 ) = ( 𝑧 ( Hom ‘ ( SetCat ‘ 2o ) ) 𝑤 ) )
28 26 27 ineq12d ⊢ ( ℎ = ( Hom ‘ ( SetCat ‘ 2o ) ) → ( ( 𝑥 ℎ 𝑦 ) ∩ ( 𝑧 ℎ 𝑤 ) ) = ( ( 𝑥 ( Hom ‘ ( SetCat ‘ 2o ) ) 𝑦 ) ∩ ( 𝑧 ( Hom ‘ ( SetCat ‘ 2o ) ) 𝑤 ) ) )
29 28 neeq1d ⊢ ( ℎ = ( Hom ‘ ( SetCat ‘ 2o ) ) → ( ( ( 𝑥 ℎ 𝑦 ) ∩ ( 𝑧 ℎ 𝑤 ) ) ≠ ∅ ↔ ( ( 𝑥 ( Hom ‘ ( SetCat ‘ 2o ) ) 𝑦 ) ∩ ( 𝑧 ( Hom ‘ ( SetCat ‘ 2o ) ) 𝑤 ) ) ≠ ∅ ) )
30 29 anbi1d ⊢ ( ℎ = ( Hom ‘ ( SetCat ‘ 2o ) ) → ( ( ( ( 𝑥 ℎ 𝑦 ) ∩ ( 𝑧 ℎ 𝑤 ) ) ≠ ∅ ∧ ¬ ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ↔ ( ( ( 𝑥 ( Hom ‘ ( SetCat ‘ 2o ) ) 𝑦 ) ∩ ( 𝑧 ( Hom ‘ ( SetCat ‘ 2o ) ) 𝑤 ) ) ≠ ∅ ∧ ¬ ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ) )
31 30 2rexbidv ⊢ ( ℎ = ( Hom ‘ ( SetCat ‘ 2o ) ) → ( ∃ 𝑧 ∈ 𝑏 ∃ 𝑤 ∈ 𝑏 ( ( ( 𝑥 ℎ 𝑦 ) ∩ ( 𝑧 ℎ 𝑤 ) ) ≠ ∅ ∧ ¬ ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ↔ ∃ 𝑧 ∈ 𝑏 ∃ 𝑤 ∈ 𝑏 ( ( ( 𝑥 ( Hom ‘ ( SetCat ‘ 2o ) ) 𝑦 ) ∩ ( 𝑧 ( Hom ‘ ( SetCat ‘ 2o ) ) 𝑤 ) ) ≠ ∅ ∧ ¬ ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ) )
32 31 2rexbidv ⊢ ( ℎ = ( Hom ‘ ( SetCat ‘ 2o ) ) → ( ∃ 𝑥 ∈ 𝑏 ∃ 𝑦 ∈ 𝑏 ∃ 𝑧 ∈ 𝑏 ∃ 𝑤 ∈ 𝑏 ( ( ( 𝑥 ℎ 𝑦 ) ∩ ( 𝑧 ℎ 𝑤 ) ) ≠ ∅ ∧ ¬ ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ↔ ∃ 𝑥 ∈ 𝑏 ∃ 𝑦 ∈ 𝑏 ∃ 𝑧 ∈ 𝑏 ∃ 𝑤 ∈ 𝑏 ( ( ( 𝑥 ( Hom ‘ ( SetCat ‘ 2o ) ) 𝑦 ) ∩ ( 𝑧 ( Hom ‘ ( SetCat ‘ 2o ) ) 𝑤 ) ) ≠ ∅ ∧ ¬ ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ) )
33 32 adantl ⊢ ( ( ( 𝑐 = ( SetCat ‘ 2o ) ∧ 𝑏 = ( Base ‘ ( SetCat ‘ 2o ) ) ) ∧ ℎ = ( Hom ‘ ( SetCat ‘ 2o ) ) ) → ( ∃ 𝑥 ∈ 𝑏 ∃ 𝑦 ∈ 𝑏 ∃ 𝑧 ∈ 𝑏 ∃ 𝑤 ∈ 𝑏 ( ( ( 𝑥 ℎ 𝑦 ) ∩ ( 𝑧 ℎ 𝑤 ) ) ≠ ∅ ∧ ¬ ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ↔ ∃ 𝑥 ∈ 𝑏 ∃ 𝑦 ∈ 𝑏 ∃ 𝑧 ∈ 𝑏 ∃ 𝑤 ∈ 𝑏 ( ( ( 𝑥 ( Hom ‘ ( SetCat ‘ 2o ) ) 𝑦 ) ∩ ( 𝑧 ( Hom ‘ ( SetCat ‘ 2o ) ) 𝑤 ) ) ≠ ∅ ∧ ¬ ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ) )
34 pm4.61 ⊢ ( ¬ ( ( ( 𝑥 ℎ 𝑦 ) ∩ ( 𝑧 ℎ 𝑤 ) ) ≠ ∅ → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ↔ ( ( ( 𝑥 ℎ 𝑦 ) ∩ ( 𝑧 ℎ 𝑤 ) ) ≠ ∅ ∧ ¬ ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) )
35 34 2rexbii ⊢ ( ∃ 𝑧 ∈ 𝑏 ∃ 𝑤 ∈ 𝑏 ¬ ( ( ( 𝑥 ℎ 𝑦 ) ∩ ( 𝑧 ℎ 𝑤 ) ) ≠ ∅ → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ↔ ∃ 𝑧 ∈ 𝑏 ∃ 𝑤 ∈ 𝑏 ( ( ( 𝑥 ℎ 𝑦 ) ∩ ( 𝑧 ℎ 𝑤 ) ) ≠ ∅ ∧ ¬ ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) )
36 rexnal2 ⊢ ( ∃ 𝑧 ∈ 𝑏 ∃ 𝑤 ∈ 𝑏 ¬ ( ( ( 𝑥 ℎ 𝑦 ) ∩ ( 𝑧 ℎ 𝑤 ) ) ≠ ∅ → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ↔ ¬ ∀ 𝑧 ∈ 𝑏 ∀ 𝑤 ∈ 𝑏 ( ( ( 𝑥 ℎ 𝑦 ) ∩ ( 𝑧 ℎ 𝑤 ) ) ≠ ∅ → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) )
37 35 36 bitr3i ⊢ ( ∃ 𝑧 ∈ 𝑏 ∃ 𝑤 ∈ 𝑏 ( ( ( 𝑥 ℎ 𝑦 ) ∩ ( 𝑧 ℎ 𝑤 ) ) ≠ ∅ ∧ ¬ ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ↔ ¬ ∀ 𝑧 ∈ 𝑏 ∀ 𝑤 ∈ 𝑏 ( ( ( 𝑥 ℎ 𝑦 ) ∩ ( 𝑧 ℎ 𝑤 ) ) ≠ ∅ → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) )
38 37 2rexbii ⊢ ( ∃ 𝑥 ∈ 𝑏 ∃ 𝑦 ∈ 𝑏 ∃ 𝑧 ∈ 𝑏 ∃ 𝑤 ∈ 𝑏 ( ( ( 𝑥 ℎ 𝑦 ) ∩ ( 𝑧 ℎ 𝑤 ) ) ≠ ∅ ∧ ¬ ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ↔ ∃ 𝑥 ∈ 𝑏 ∃ 𝑦 ∈ 𝑏 ¬ ∀ 𝑧 ∈ 𝑏 ∀ 𝑤 ∈ 𝑏 ( ( ( 𝑥 ℎ 𝑦 ) ∩ ( 𝑧 ℎ 𝑤 ) ) ≠ ∅ → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) )
39 rexnal2 ⊢ ( ∃ 𝑥 ∈ 𝑏 ∃ 𝑦 ∈ 𝑏 ¬ ∀ 𝑧 ∈ 𝑏 ∀ 𝑤 ∈ 𝑏 ( ( ( 𝑥 ℎ 𝑦 ) ∩ ( 𝑧 ℎ 𝑤 ) ) ≠ ∅ → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ↔ ¬ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ∀ 𝑤 ∈ 𝑏 ( ( ( 𝑥 ℎ 𝑦 ) ∩ ( 𝑧 ℎ 𝑤 ) ) ≠ ∅ → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) )
40 38 39 bitri ⊢ ( ∃ 𝑥 ∈ 𝑏 ∃ 𝑦 ∈ 𝑏 ∃ 𝑧 ∈ 𝑏 ∃ 𝑤 ∈ 𝑏 ( ( ( 𝑥 ℎ 𝑦 ) ∩ ( 𝑧 ℎ 𝑤 ) ) ≠ ∅ ∧ ¬ ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ↔ ¬ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ∀ 𝑤 ∈ 𝑏 ( ( ( 𝑥 ℎ 𝑦 ) ∩ ( 𝑧 ℎ 𝑤 ) ) ≠ ∅ → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) )
41 40 a1i ⊢ ( ( ( 𝑐 = ( SetCat ‘ 2o ) ∧ 𝑏 = ( Base ‘ ( SetCat ‘ 2o ) ) ) ∧ ℎ = ( Hom ‘ ( SetCat ‘ 2o ) ) ) → ( ∃ 𝑥 ∈ 𝑏 ∃ 𝑦 ∈ 𝑏 ∃ 𝑧 ∈ 𝑏 ∃ 𝑤 ∈ 𝑏 ( ( ( 𝑥 ℎ 𝑦 ) ∩ ( 𝑧 ℎ 𝑤 ) ) ≠ ∅ ∧ ¬ ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ↔ ¬ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ∀ 𝑤 ∈ 𝑏 ( ( ( 𝑥 ℎ 𝑦 ) ∩ ( 𝑧 ℎ 𝑤 ) ) ≠ ∅ → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ) )
42 rexeq ⊢ ( 𝑏 = ( Base ‘ ( SetCat ‘ 2o ) ) → ( ∃ 𝑤 ∈ 𝑏 ( ( ( 𝑥 ( Hom ‘ ( SetCat ‘ 2o ) ) 𝑦 ) ∩ ( 𝑧 ( Hom ‘ ( SetCat ‘ 2o ) ) 𝑤 ) ) ≠ ∅ ∧ ¬ ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ↔ ∃ 𝑤 ∈ ( Base ‘ ( SetCat ‘ 2o ) ) ( ( ( 𝑥 ( Hom ‘ ( SetCat ‘ 2o ) ) 𝑦 ) ∩ ( 𝑧 ( Hom ‘ ( SetCat ‘ 2o ) ) 𝑤 ) ) ≠ ∅ ∧ ¬ ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ) )
43 42 2rexbidv ⊢ ( 𝑏 = ( Base ‘ ( SetCat ‘ 2o ) ) → ( ∃ 𝑦 ∈ 𝑏 ∃ 𝑧 ∈ 𝑏 ∃ 𝑤 ∈ 𝑏 ( ( ( 𝑥 ( Hom ‘ ( SetCat ‘ 2o ) ) 𝑦 ) ∩ ( 𝑧 ( Hom ‘ ( SetCat ‘ 2o ) ) 𝑤 ) ) ≠ ∅ ∧ ¬ ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ↔ ∃ 𝑦 ∈ 𝑏 ∃ 𝑧 ∈ 𝑏 ∃ 𝑤 ∈ ( Base ‘ ( SetCat ‘ 2o ) ) ( ( ( 𝑥 ( Hom ‘ ( SetCat ‘ 2o ) ) 𝑦 ) ∩ ( 𝑧 ( Hom ‘ ( SetCat ‘ 2o ) ) 𝑤 ) ) ≠ ∅ ∧ ¬ ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ) )
44 43 rexbidv ⊢ ( 𝑏 = ( Base ‘ ( SetCat ‘ 2o ) ) → ( ∃ 𝑥 ∈ 𝑏 ∃ 𝑦 ∈ 𝑏 ∃ 𝑧 ∈ 𝑏 ∃ 𝑤 ∈ 𝑏 ( ( ( 𝑥 ( Hom ‘ ( SetCat ‘ 2o ) ) 𝑦 ) ∩ ( 𝑧 ( Hom ‘ ( SetCat ‘ 2o ) ) 𝑤 ) ) ≠ ∅ ∧ ¬ ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ↔ ∃ 𝑥 ∈ 𝑏 ∃ 𝑦 ∈ 𝑏 ∃ 𝑧 ∈ 𝑏 ∃ 𝑤 ∈ ( Base ‘ ( SetCat ‘ 2o ) ) ( ( ( 𝑥 ( Hom ‘ ( SetCat ‘ 2o ) ) 𝑦 ) ∩ ( 𝑧 ( Hom ‘ ( SetCat ‘ 2o ) ) 𝑤 ) ) ≠ ∅ ∧ ¬ ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ) )
45 rexeq ⊢ ( 𝑏 = ( 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 ⊢ ( 𝑏 = ( 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 ⊢ ( 𝑏 = ( 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 ⊢ ( 𝑏 = ( 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 ⊢ ( 𝑏 = ( 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 ⊢ ( ( ( 𝑐 = ( 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 ⊢ ( ( ( 𝑐 = ( 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 ⊢ ( ( 𝑐 = ( 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 ⊢ ( 𝑐 = ( 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 ⊢ ( ( ( 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 ⊢ ∃ 𝑐 ∈ Cat [ ( Base ‘ 𝑐 ) / 𝑏 ] [ ( Hom ‘ 𝑐 ) / ℎ ] ¬ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∀ 𝑧 ∈ 𝑏 ∀ 𝑤 ∈ 𝑏 ( ( ( 𝑥 ℎ 𝑦 ) ∩ ( 𝑧 ℎ 𝑤 ) ) ≠ ∅ → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) )