Metamath Proof Explorer


Theorem catcoppcclOLD

Description: Obsolete proof of catcoppccl as of 13-Oct-2024. (Contributed by Mario Carneiro, 12-Jan-2017) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses catcoppccl.c 𝐶 = ( CatCat ‘ 𝑈 )
catcoppccl.b 𝐵 = ( Base ‘ 𝐶 )
catcoppccl.o 𝑂 = ( oppCat ‘ 𝑋 )
catcoppccl.1 ( 𝜑𝑈 ∈ WUni )
catcoppccl.2 ( 𝜑 → ω ∈ 𝑈 )
catcoppccl.3 ( 𝜑𝑋𝐵 )
Assertion catcoppcclOLD ( 𝜑𝑂𝐵 )

Proof

Step Hyp Ref Expression
1 catcoppccl.c 𝐶 = ( CatCat ‘ 𝑈 )
2 catcoppccl.b 𝐵 = ( Base ‘ 𝐶 )
3 catcoppccl.o 𝑂 = ( oppCat ‘ 𝑋 )
4 catcoppccl.1 ( 𝜑𝑈 ∈ WUni )
5 catcoppccl.2 ( 𝜑 → ω ∈ 𝑈 )
6 catcoppccl.3 ( 𝜑𝑋𝐵 )
7 eqid ( Base ‘ 𝑋 ) = ( Base ‘ 𝑋 )
8 eqid ( Hom ‘ 𝑋 ) = ( Hom ‘ 𝑋 )
9 eqid ( comp ‘ 𝑋 ) = ( comp ‘ 𝑋 )
10 7 8 9 3 oppcval ( 𝑋𝐵𝑂 = ( ( 𝑋 sSet ⟨ ( Hom ‘ ndx ) , tpos ( Hom ‘ 𝑋 ) ⟩ ) sSet ⟨ ( comp ‘ ndx ) , ( 𝑥 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑋 ) ) , 𝑦 ∈ ( Base ‘ 𝑋 ) ↦ tpos ( ⟨ 𝑦 , ( 2nd𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1st𝑥 ) ) ) ⟩ ) )
11 6 10 syl ( 𝜑𝑂 = ( ( 𝑋 sSet ⟨ ( Hom ‘ ndx ) , tpos ( Hom ‘ 𝑋 ) ⟩ ) sSet ⟨ ( comp ‘ ndx ) , ( 𝑥 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑋 ) ) , 𝑦 ∈ ( Base ‘ 𝑋 ) ↦ tpos ( ⟨ 𝑦 , ( 2nd𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1st𝑥 ) ) ) ⟩ ) )
12 1 2 4 catcbas ( 𝜑𝐵 = ( 𝑈 ∩ Cat ) )
13 6 12 eleqtrd ( 𝜑𝑋 ∈ ( 𝑈 ∩ Cat ) )
14 13 elin1d ( 𝜑𝑋𝑈 )
15 df-hom Hom = Slot 1 4
16 4 5 wunndx ( 𝜑 → ndx ∈ 𝑈 )
17 15 4 16 wunstr ( 𝜑 → ( Hom ‘ ndx ) ∈ 𝑈 )
18 15 4 14 wunstr ( 𝜑 → ( Hom ‘ 𝑋 ) ∈ 𝑈 )
19 4 18 wuntpos ( 𝜑 → tpos ( Hom ‘ 𝑋 ) ∈ 𝑈 )
20 4 17 19 wunop ( 𝜑 → ⟨ ( Hom ‘ ndx ) , tpos ( Hom ‘ 𝑋 ) ⟩ ∈ 𝑈 )
21 4 14 20 wunsets ( 𝜑 → ( 𝑋 sSet ⟨ ( Hom ‘ ndx ) , tpos ( Hom ‘ 𝑋 ) ⟩ ) ∈ 𝑈 )
22 df-cco comp = Slot 1 5
23 22 4 16 wunstr ( 𝜑 → ( comp ‘ ndx ) ∈ 𝑈 )
24 df-base Base = Slot 1
25 24 4 14 wunstr ( 𝜑 → ( Base ‘ 𝑋 ) ∈ 𝑈 )
26 4 25 25 wunxp ( 𝜑 → ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑋 ) ) ∈ 𝑈 )
27 4 26 25 wunxp ( 𝜑 → ( ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑋 ) ) × ( Base ‘ 𝑋 ) ) ∈ 𝑈 )
28 22 4 14 wunstr ( 𝜑 → ( comp ‘ 𝑋 ) ∈ 𝑈 )
29 4 28 wunrn ( 𝜑 → ran ( comp ‘ 𝑋 ) ∈ 𝑈 )
30 4 29 wununi ( 𝜑 ran ( comp ‘ 𝑋 ) ∈ 𝑈 )
31 4 30 wundm ( 𝜑 → dom ran ( comp ‘ 𝑋 ) ∈ 𝑈 )
32 4 31 wuncnv ( 𝜑 dom ran ( comp ‘ 𝑋 ) ∈ 𝑈 )
33 4 wun0 ( 𝜑 → ∅ ∈ 𝑈 )
34 4 33 wunsn ( 𝜑 → { ∅ } ∈ 𝑈 )
35 4 32 34 wunun ( 𝜑 → ( dom ran ( comp ‘ 𝑋 ) ∪ { ∅ } ) ∈ 𝑈 )
36 4 30 wunrn ( 𝜑 → ran ran ( comp ‘ 𝑋 ) ∈ 𝑈 )
37 4 35 36 wunxp ( 𝜑 → ( ( dom ran ( comp ‘ 𝑋 ) ∪ { ∅ } ) × ran ran ( comp ‘ 𝑋 ) ) ∈ 𝑈 )
38 4 37 wunpw ( 𝜑 → 𝒫 ( ( dom ran ( comp ‘ 𝑋 ) ∪ { ∅ } ) × ran ran ( comp ‘ 𝑋 ) ) ∈ 𝑈 )
39 tposssxp tpos ( ⟨ 𝑦 , ( 2nd𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1st𝑥 ) ) ⊆ ( ( dom ( ⟨ 𝑦 , ( 2nd𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1st𝑥 ) ) ∪ { ∅ } ) × ran ( ⟨ 𝑦 , ( 2nd𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1st𝑥 ) ) )
40 ovssunirn ( ⟨ 𝑦 , ( 2nd𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1st𝑥 ) ) ⊆ ran ( comp ‘ 𝑋 )
41 dmss ( ( ⟨ 𝑦 , ( 2nd𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1st𝑥 ) ) ⊆ ran ( comp ‘ 𝑋 ) → dom ( ⟨ 𝑦 , ( 2nd𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1st𝑥 ) ) ⊆ dom ran ( comp ‘ 𝑋 ) )
42 40 41 ax-mp dom ( ⟨ 𝑦 , ( 2nd𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1st𝑥 ) ) ⊆ dom ran ( comp ‘ 𝑋 )
43 cnvss ( dom ( ⟨ 𝑦 , ( 2nd𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1st𝑥 ) ) ⊆ dom ran ( comp ‘ 𝑋 ) → dom ( ⟨ 𝑦 , ( 2nd𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1st𝑥 ) ) ⊆ dom ran ( comp ‘ 𝑋 ) )
44 unss1 ( dom ( ⟨ 𝑦 , ( 2nd𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1st𝑥 ) ) ⊆ dom ran ( comp ‘ 𝑋 ) → ( dom ( ⟨ 𝑦 , ( 2nd𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1st𝑥 ) ) ∪ { ∅ } ) ⊆ ( dom ran ( comp ‘ 𝑋 ) ∪ { ∅ } ) )
45 42 43 44 mp2b ( dom ( ⟨ 𝑦 , ( 2nd𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1st𝑥 ) ) ∪ { ∅ } ) ⊆ ( dom ran ( comp ‘ 𝑋 ) ∪ { ∅ } )
46 40 rnssi ran ( ⟨ 𝑦 , ( 2nd𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1st𝑥 ) ) ⊆ ran ran ( comp ‘ 𝑋 )
47 xpss12 ( ( ( dom ( ⟨ 𝑦 , ( 2nd𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1st𝑥 ) ) ∪ { ∅ } ) ⊆ ( dom ran ( comp ‘ 𝑋 ) ∪ { ∅ } ) ∧ ran ( ⟨ 𝑦 , ( 2nd𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1st𝑥 ) ) ⊆ ran ran ( comp ‘ 𝑋 ) ) → ( ( dom ( ⟨ 𝑦 , ( 2nd𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1st𝑥 ) ) ∪ { ∅ } ) × ran ( ⟨ 𝑦 , ( 2nd𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1st𝑥 ) ) ) ⊆ ( ( dom ran ( comp ‘ 𝑋 ) ∪ { ∅ } ) × ran ran ( comp ‘ 𝑋 ) ) )
48 45 46 47 mp2an ( ( dom ( ⟨ 𝑦 , ( 2nd𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1st𝑥 ) ) ∪ { ∅ } ) × ran ( ⟨ 𝑦 , ( 2nd𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1st𝑥 ) ) ) ⊆ ( ( dom ran ( comp ‘ 𝑋 ) ∪ { ∅ } ) × ran ran ( comp ‘ 𝑋 ) )
49 39 48 sstri tpos ( ⟨ 𝑦 , ( 2nd𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1st𝑥 ) ) ⊆ ( ( dom ran ( comp ‘ 𝑋 ) ∪ { ∅ } ) × ran ran ( comp ‘ 𝑋 ) )
50 elpw2g ( ( ( dom ran ( comp ‘ 𝑋 ) ∪ { ∅ } ) × ran ran ( comp ‘ 𝑋 ) ) ∈ 𝑈 → ( tpos ( ⟨ 𝑦 , ( 2nd𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1st𝑥 ) ) ∈ 𝒫 ( ( dom ran ( comp ‘ 𝑋 ) ∪ { ∅ } ) × ran ran ( comp ‘ 𝑋 ) ) ↔ tpos ( ⟨ 𝑦 , ( 2nd𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1st𝑥 ) ) ⊆ ( ( dom ran ( comp ‘ 𝑋 ) ∪ { ∅ } ) × ran ran ( comp ‘ 𝑋 ) ) ) )
51 37 50 syl ( 𝜑 → ( tpos ( ⟨ 𝑦 , ( 2nd𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1st𝑥 ) ) ∈ 𝒫 ( ( dom ran ( comp ‘ 𝑋 ) ∪ { ∅ } ) × ran ran ( comp ‘ 𝑋 ) ) ↔ tpos ( ⟨ 𝑦 , ( 2nd𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1st𝑥 ) ) ⊆ ( ( dom ran ( comp ‘ 𝑋 ) ∪ { ∅ } ) × ran ran ( comp ‘ 𝑋 ) ) ) )
52 49 51 mpbiri ( 𝜑 → tpos ( ⟨ 𝑦 , ( 2nd𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1st𝑥 ) ) ∈ 𝒫 ( ( dom ran ( comp ‘ 𝑋 ) ∪ { ∅ } ) × ran ran ( comp ‘ 𝑋 ) ) )
53 52 ralrimivw ( 𝜑 → ∀ 𝑦 ∈ ( Base ‘ 𝑋 ) tpos ( ⟨ 𝑦 , ( 2nd𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1st𝑥 ) ) ∈ 𝒫 ( ( dom ran ( comp ‘ 𝑋 ) ∪ { ∅ } ) × ran ran ( comp ‘ 𝑋 ) ) )
54 53 ralrimivw ( 𝜑 → ∀ 𝑥 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑋 ) ) ∀ 𝑦 ∈ ( Base ‘ 𝑋 ) tpos ( ⟨ 𝑦 , ( 2nd𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1st𝑥 ) ) ∈ 𝒫 ( ( dom ran ( comp ‘ 𝑋 ) ∪ { ∅ } ) × ran ran ( comp ‘ 𝑋 ) ) )
55 eqid ( 𝑥 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑋 ) ) , 𝑦 ∈ ( Base ‘ 𝑋 ) ↦ tpos ( ⟨ 𝑦 , ( 2nd𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1st𝑥 ) ) ) = ( 𝑥 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑋 ) ) , 𝑦 ∈ ( Base ‘ 𝑋 ) ↦ tpos ( ⟨ 𝑦 , ( 2nd𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1st𝑥 ) ) )
56 55 fmpo ( ∀ 𝑥 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑋 ) ) ∀ 𝑦 ∈ ( Base ‘ 𝑋 ) tpos ( ⟨ 𝑦 , ( 2nd𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1st𝑥 ) ) ∈ 𝒫 ( ( dom ran ( comp ‘ 𝑋 ) ∪ { ∅ } ) × ran ran ( comp ‘ 𝑋 ) ) ↔ ( 𝑥 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑋 ) ) , 𝑦 ∈ ( Base ‘ 𝑋 ) ↦ tpos ( ⟨ 𝑦 , ( 2nd𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1st𝑥 ) ) ) : ( ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑋 ) ) × ( Base ‘ 𝑋 ) ) ⟶ 𝒫 ( ( dom ran ( comp ‘ 𝑋 ) ∪ { ∅ } ) × ran ran ( comp ‘ 𝑋 ) ) )
57 54 56 sylib ( 𝜑 → ( 𝑥 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑋 ) ) , 𝑦 ∈ ( Base ‘ 𝑋 ) ↦ tpos ( ⟨ 𝑦 , ( 2nd𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1st𝑥 ) ) ) : ( ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑋 ) ) × ( Base ‘ 𝑋 ) ) ⟶ 𝒫 ( ( dom ran ( comp ‘ 𝑋 ) ∪ { ∅ } ) × ran ran ( comp ‘ 𝑋 ) ) )
58 4 27 38 57 wunf ( 𝜑 → ( 𝑥 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑋 ) ) , 𝑦 ∈ ( Base ‘ 𝑋 ) ↦ tpos ( ⟨ 𝑦 , ( 2nd𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1st𝑥 ) ) ) ∈ 𝑈 )
59 4 23 58 wunop ( 𝜑 → ⟨ ( comp ‘ ndx ) , ( 𝑥 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑋 ) ) , 𝑦 ∈ ( Base ‘ 𝑋 ) ↦ tpos ( ⟨ 𝑦 , ( 2nd𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1st𝑥 ) ) ) ⟩ ∈ 𝑈 )
60 4 21 59 wunsets ( 𝜑 → ( ( 𝑋 sSet ⟨ ( Hom ‘ ndx ) , tpos ( Hom ‘ 𝑋 ) ⟩ ) sSet ⟨ ( comp ‘ ndx ) , ( 𝑥 ∈ ( ( Base ‘ 𝑋 ) × ( Base ‘ 𝑋 ) ) , 𝑦 ∈ ( Base ‘ 𝑋 ) ↦ tpos ( ⟨ 𝑦 , ( 2nd𝑥 ) ⟩ ( comp ‘ 𝑋 ) ( 1st𝑥 ) ) ) ⟩ ) ∈ 𝑈 )
61 11 60 eqeltrd ( 𝜑𝑂𝑈 )
62 13 elin2d ( 𝜑𝑋 ∈ Cat )
63 3 oppccat ( 𝑋 ∈ Cat → 𝑂 ∈ Cat )
64 62 63 syl ( 𝜑𝑂 ∈ Cat )
65 61 64 elind ( 𝜑𝑂 ∈ ( 𝑈 ∩ Cat ) )
66 65 12 eleqtrrd ( 𝜑𝑂𝐵 )