Metamath Proof Explorer

Theorem thincciso

Description: Two thin categories are isomorphic iff the induced preorders are order-isomorphic. Example 3.26(2) of Adamek p. 33. Note that "thincciso.u" is redundant thanks to elbasfv . (Contributed by Zhi Wang, 16-Oct-2024)

Ref Expression
Hypotheses thincciso.c ⊢ 𝐶 = ( CatCat ‘ 𝑈 )
thincciso.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
thincciso.r ⊢ 𝑅 = ( Base ‘ 𝑋 )
thincciso.s ⊢ 𝑆 = ( Base ‘ 𝑌 )
thincciso.h ⊢ 𝐻 = ( Hom ‘ 𝑋 )
thincciso.j ⊢ 𝐽 = ( Hom ‘ 𝑌 )
thincciso.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
thincciso.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
thincciso.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
thincciso.xt ⊢ ( 𝜑 → 𝑋 ∈ ThinCat )
thincciso.yt ⊢ ( 𝜑 → 𝑌 ∈ ThinCat )
Assertion thincciso ( 𝜑 → ( 𝑋 ( ≃𝑐 ‘ 𝐶 ) 𝑌 ↔ ∃ 𝑓 ( ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( ( 𝑥 𝐻 𝑦 ) = ∅ ↔ ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) = ∅ ) ∧ 𝑓 : 𝑅 –1-1-onto→ 𝑆 ) ) )

Proof

Step Hyp Ref Expression
1 thincciso.c ⊢ 𝐶 = ( CatCat ‘ 𝑈 )
2 thincciso.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
3 thincciso.r ⊢ 𝑅 = ( Base ‘ 𝑋 )
4 thincciso.s ⊢ 𝑆 = ( Base ‘ 𝑌 )
5 thincciso.h ⊢ 𝐻 = ( Hom ‘ 𝑋 )
6 thincciso.j ⊢ 𝐽 = ( Hom ‘ 𝑌 )
7 thincciso.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
8 thincciso.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
9 thincciso.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
10 thincciso.xt ⊢ ( 𝜑 → 𝑋 ∈ ThinCat )
11 thincciso.yt ⊢ ( 𝜑 → 𝑌 ∈ ThinCat )
12 eqid ⊢ ( Iso ‘ 𝐶 ) = ( Iso ‘ 𝐶 )
13 1 catccat ⊢ ( 𝑈 ∈ 𝑉 → 𝐶 ∈ Cat )
14 7 13 syl ⊢ ( 𝜑 → 𝐶 ∈ Cat )
15 12 2 14 8 9 cic ⊢ ( 𝜑 → ( 𝑋 ( ≃𝑐 ‘ 𝐶 ) 𝑌 ↔ ∃ 𝑎 𝑎 ∈ ( 𝑋 ( Iso ‘ 𝐶 ) 𝑌 ) ) )
16 opex ⊢ ⟨ 𝑓 , ( 𝑧 ∈ 𝑅 , 𝑤 ∈ 𝑅 ↦ ( ( 𝑧 𝐻 𝑤 ) × ( ( 𝑓 ‘ 𝑧 ) 𝐽 ( 𝑓 ‘ 𝑤 ) ) ) ) ⟩ ∈ V
17 16 a1i ⊢ ( ( 𝜑 ∧ ( ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( ( 𝑥 𝐻 𝑦 ) = ∅ ↔ ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) = ∅ ) ∧ 𝑓 : 𝑅 –1-1-onto→ 𝑆 ) ) → ⟨ 𝑓 , ( 𝑧 ∈ 𝑅 , 𝑤 ∈ 𝑅 ↦ ( ( 𝑧 𝐻 𝑤 ) × ( ( 𝑓 ‘ 𝑧 ) 𝐽 ( 𝑓 ‘ 𝑤 ) ) ) ) ⟩ ∈ V )
18 biimp ⊢ ( ( ( 𝑥 𝐻 𝑦 ) = ∅ ↔ ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) = ∅ ) → ( ( 𝑥 𝐻 𝑦 ) = ∅ → ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) = ∅ ) )
19 18 2ralimi ⊢ ( ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( ( 𝑥 𝐻 𝑦 ) = ∅ ↔ ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) = ∅ ) → ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( ( 𝑥 𝐻 𝑦 ) = ∅ → ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) = ∅ ) )
20 19 ad2antrl ⊢ ( ( 𝜑 ∧ ( ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( ( 𝑥 𝐻 𝑦 ) = ∅ ↔ ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) = ∅ ) ∧ 𝑓 : 𝑅 –1-1-onto→ 𝑆 ) ) → ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( ( 𝑥 𝐻 𝑦 ) = ∅ → ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) = ∅ ) )
21 11 adantr ⊢ ( ( 𝜑 ∧ ( ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( ( 𝑥 𝐻 𝑦 ) = ∅ ↔ ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) = ∅ ) ∧ 𝑓 : 𝑅 –1-1-onto→ 𝑆 ) ) → 𝑌 ∈ ThinCat )
22 eqid ⊢ ( 𝑧 ∈ 𝑅 , 𝑤 ∈ 𝑅 ↦ ( ( 𝑧 𝐻 𝑤 ) × ( ( 𝑓 ‘ 𝑧 ) 𝐽 ( 𝑓 ‘ 𝑤 ) ) ) ) = ( 𝑧 ∈ 𝑅 , 𝑤 ∈ 𝑅 ↦ ( ( 𝑧 𝐻 𝑤 ) × ( ( 𝑓 ‘ 𝑧 ) 𝐽 ( 𝑓 ‘ 𝑤 ) ) ) )
23 10 adantr ⊢ ( ( 𝜑 ∧ ( ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( ( 𝑥 𝐻 𝑦 ) = ∅ ↔ ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) = ∅ ) ∧ 𝑓 : 𝑅 –1-1-onto→ 𝑆 ) ) → 𝑋 ∈ ThinCat )
24 23 thinccatd ⊢ ( ( 𝜑 ∧ ( ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( ( 𝑥 𝐻 𝑦 ) = ∅ ↔ ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) = ∅ ) ∧ 𝑓 : 𝑅 –1-1-onto→ 𝑆 ) ) → 𝑋 ∈ Cat )
25 simprr ⊢ ( ( 𝜑 ∧ ( ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( ( 𝑥 𝐻 𝑦 ) = ∅ ↔ ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) = ∅ ) ∧ 𝑓 : 𝑅 –1-1-onto→ 𝑆 ) ) → 𝑓 : 𝑅 –1-1-onto→ 𝑆 )
26 f1of ⊢ ( 𝑓 : 𝑅 –1-1-onto→ 𝑆 → 𝑓 : 𝑅 ⟶ 𝑆 )
27 25 26 syl ⊢ ( ( 𝜑 ∧ ( ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( ( 𝑥 𝐻 𝑦 ) = ∅ ↔ ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) = ∅ ) ∧ 𝑓 : 𝑅 –1-1-onto→ 𝑆 ) ) → 𝑓 : 𝑅 ⟶ 𝑆 )
28 biimpr ⊢ ( ( ( 𝑥 𝐻 𝑦 ) = ∅ ↔ ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) = ∅ ) → ( ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) = ∅ → ( 𝑥 𝐻 𝑦 ) = ∅ ) )
29 28 2ralimi ⊢ ( ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( ( 𝑥 𝐻 𝑦 ) = ∅ ↔ ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) = ∅ ) → ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) = ∅ → ( 𝑥 𝐻 𝑦 ) = ∅ ) )
30 29 ad2antrl ⊢ ( ( 𝜑 ∧ ( ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( ( 𝑥 𝐻 𝑦 ) = ∅ ↔ ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) = ∅ ) ∧ 𝑓 : 𝑅 –1-1-onto→ 𝑆 ) ) → ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) = ∅ → ( 𝑥 𝐻 𝑦 ) = ∅ ) )
31 3 4 5 6 24 21 27 22 30 functhinc ⊢ ( ( 𝜑 ∧ ( ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( ( 𝑥 𝐻 𝑦 ) = ∅ ↔ ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) = ∅ ) ∧ 𝑓 : 𝑅 –1-1-onto→ 𝑆 ) ) → ( 𝑓 ( 𝑋 Func 𝑌 ) ( 𝑧 ∈ 𝑅 , 𝑤 ∈ 𝑅 ↦ ( ( 𝑧 𝐻 𝑤 ) × ( ( 𝑓 ‘ 𝑧 ) 𝐽 ( 𝑓 ‘ 𝑤 ) ) ) ) ↔ ( 𝑧 ∈ 𝑅 , 𝑤 ∈ 𝑅 ↦ ( ( 𝑧 𝐻 𝑤 ) × ( ( 𝑓 ‘ 𝑧 ) 𝐽 ( 𝑓 ‘ 𝑤 ) ) ) ) = ( 𝑧 ∈ 𝑅 , 𝑤 ∈ 𝑅 ↦ ( ( 𝑧 𝐻 𝑤 ) × ( ( 𝑓 ‘ 𝑧 ) 𝐽 ( 𝑓 ‘ 𝑤 ) ) ) ) ) )
32 22 31 mpbiri ⊢ ( ( 𝜑 ∧ ( ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( ( 𝑥 𝐻 𝑦 ) = ∅ ↔ ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) = ∅ ) ∧ 𝑓 : 𝑅 –1-1-onto→ 𝑆 ) ) → 𝑓 ( 𝑋 Func 𝑌 ) ( 𝑧 ∈ 𝑅 , 𝑤 ∈ 𝑅 ↦ ( ( 𝑧 𝐻 𝑤 ) × ( ( 𝑓 ‘ 𝑧 ) 𝐽 ( 𝑓 ‘ 𝑤 ) ) ) ) )
33 3 6 5 21 32 fullthinc ⊢ ( ( 𝜑 ∧ ( ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( ( 𝑥 𝐻 𝑦 ) = ∅ ↔ ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) = ∅ ) ∧ 𝑓 : 𝑅 –1-1-onto→ 𝑆 ) ) → ( 𝑓 ( 𝑋 Full 𝑌 ) ( 𝑧 ∈ 𝑅 , 𝑤 ∈ 𝑅 ↦ ( ( 𝑧 𝐻 𝑤 ) × ( ( 𝑓 ‘ 𝑧 ) 𝐽 ( 𝑓 ‘ 𝑤 ) ) ) ) ↔ ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( ( 𝑥 𝐻 𝑦 ) = ∅ → ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) = ∅ ) ) )
34 20 33 mpbird ⊢ ( ( 𝜑 ∧ ( ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( ( 𝑥 𝐻 𝑦 ) = ∅ ↔ ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) = ∅ ) ∧ 𝑓 : 𝑅 –1-1-onto→ 𝑆 ) ) → 𝑓 ( 𝑋 Full 𝑌 ) ( 𝑧 ∈ 𝑅 , 𝑤 ∈ 𝑅 ↦ ( ( 𝑧 𝐻 𝑤 ) × ( ( 𝑓 ‘ 𝑧 ) 𝐽 ( 𝑓 ‘ 𝑤 ) ) ) ) )
35 df-br ⊢ ( 𝑓 ( 𝑋 Full 𝑌 ) ( 𝑧 ∈ 𝑅 , 𝑤 ∈ 𝑅 ↦ ( ( 𝑧 𝐻 𝑤 ) × ( ( 𝑓 ‘ 𝑧 ) 𝐽 ( 𝑓 ‘ 𝑤 ) ) ) ) ↔ ⟨ 𝑓 , ( 𝑧 ∈ 𝑅 , 𝑤 ∈ 𝑅 ↦ ( ( 𝑧 𝐻 𝑤 ) × ( ( 𝑓 ‘ 𝑧 ) 𝐽 ( 𝑓 ‘ 𝑤 ) ) ) ) ⟩ ∈ ( 𝑋 Full 𝑌 ) )
36 34 35 sylib ⊢ ( ( 𝜑 ∧ ( ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( ( 𝑥 𝐻 𝑦 ) = ∅ ↔ ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) = ∅ ) ∧ 𝑓 : 𝑅 –1-1-onto→ 𝑆 ) ) → ⟨ 𝑓 , ( 𝑧 ∈ 𝑅 , 𝑤 ∈ 𝑅 ↦ ( ( 𝑧 𝐻 𝑤 ) × ( ( 𝑓 ‘ 𝑧 ) 𝐽 ( 𝑓 ‘ 𝑤 ) ) ) ) ⟩ ∈ ( 𝑋 Full 𝑌 ) )
37 23 32 thincfth ⊢ ( ( 𝜑 ∧ ( ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( ( 𝑥 𝐻 𝑦 ) = ∅ ↔ ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) = ∅ ) ∧ 𝑓 : 𝑅 –1-1-onto→ 𝑆 ) ) → 𝑓 ( 𝑋 Faith 𝑌 ) ( 𝑧 ∈ 𝑅 , 𝑤 ∈ 𝑅 ↦ ( ( 𝑧 𝐻 𝑤 ) × ( ( 𝑓 ‘ 𝑧 ) 𝐽 ( 𝑓 ‘ 𝑤 ) ) ) ) )
38 df-br ⊢ ( 𝑓 ( 𝑋 Faith 𝑌 ) ( 𝑧 ∈ 𝑅 , 𝑤 ∈ 𝑅 ↦ ( ( 𝑧 𝐻 𝑤 ) × ( ( 𝑓 ‘ 𝑧 ) 𝐽 ( 𝑓 ‘ 𝑤 ) ) ) ) ↔ ⟨ 𝑓 , ( 𝑧 ∈ 𝑅 , 𝑤 ∈ 𝑅 ↦ ( ( 𝑧 𝐻 𝑤 ) × ( ( 𝑓 ‘ 𝑧 ) 𝐽 ( 𝑓 ‘ 𝑤 ) ) ) ) ⟩ ∈ ( 𝑋 Faith 𝑌 ) )
39 37 38 sylib ⊢ ( ( 𝜑 ∧ ( ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( ( 𝑥 𝐻 𝑦 ) = ∅ ↔ ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) = ∅ ) ∧ 𝑓 : 𝑅 –1-1-onto→ 𝑆 ) ) → ⟨ 𝑓 , ( 𝑧 ∈ 𝑅 , 𝑤 ∈ 𝑅 ↦ ( ( 𝑧 𝐻 𝑤 ) × ( ( 𝑓 ‘ 𝑧 ) 𝐽 ( 𝑓 ‘ 𝑤 ) ) ) ) ⟩ ∈ ( 𝑋 Faith 𝑌 ) )
40 36 39 elind ⊢ ( ( 𝜑 ∧ ( ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( ( 𝑥 𝐻 𝑦 ) = ∅ ↔ ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) = ∅ ) ∧ 𝑓 : 𝑅 –1-1-onto→ 𝑆 ) ) → ⟨ 𝑓 , ( 𝑧 ∈ 𝑅 , 𝑤 ∈ 𝑅 ↦ ( ( 𝑧 𝐻 𝑤 ) × ( ( 𝑓 ‘ 𝑧 ) 𝐽 ( 𝑓 ‘ 𝑤 ) ) ) ) ⟩ ∈ ( ( 𝑋 Full 𝑌 ) ∩ ( 𝑋 Faith 𝑌 ) ) )
41 vex ⊢ 𝑓 ∈ V
42 3 fvexi ⊢ 𝑅 ∈ V
43 42 42 mpoex ⊢ ( 𝑧 ∈ 𝑅 , 𝑤 ∈ 𝑅 ↦ ( ( 𝑧 𝐻 𝑤 ) × ( ( 𝑓 ‘ 𝑧 ) 𝐽 ( 𝑓 ‘ 𝑤 ) ) ) ) ∈ V
44 41 43 op1st ⊢ ( 1st ‘ ⟨ 𝑓 , ( 𝑧 ∈ 𝑅 , 𝑤 ∈ 𝑅 ↦ ( ( 𝑧 𝐻 𝑤 ) × ( ( 𝑓 ‘ 𝑧 ) 𝐽 ( 𝑓 ‘ 𝑤 ) ) ) ) ⟩ ) = 𝑓
45 f1oeq1 ⊢ ( ( 1st ‘ ⟨ 𝑓 , ( 𝑧 ∈ 𝑅 , 𝑤 ∈ 𝑅 ↦ ( ( 𝑧 𝐻 𝑤 ) × ( ( 𝑓 ‘ 𝑧 ) 𝐽 ( 𝑓 ‘ 𝑤 ) ) ) ) ⟩ ) = 𝑓 → ( ( 1st ‘ ⟨ 𝑓 , ( 𝑧 ∈ 𝑅 , 𝑤 ∈ 𝑅 ↦ ( ( 𝑧 𝐻 𝑤 ) × ( ( 𝑓 ‘ 𝑧 ) 𝐽 ( 𝑓 ‘ 𝑤 ) ) ) ) ⟩ ) : 𝑅 –1-1-onto→ 𝑆 ↔ 𝑓 : 𝑅 –1-1-onto→ 𝑆 ) )
46 44 45 ax-mp ⊢ ( ( 1st ‘ ⟨ 𝑓 , ( 𝑧 ∈ 𝑅 , 𝑤 ∈ 𝑅 ↦ ( ( 𝑧 𝐻 𝑤 ) × ( ( 𝑓 ‘ 𝑧 ) 𝐽 ( 𝑓 ‘ 𝑤 ) ) ) ) ⟩ ) : 𝑅 –1-1-onto→ 𝑆 ↔ 𝑓 : 𝑅 –1-1-onto→ 𝑆 )
47 25 46 sylibr ⊢ ( ( 𝜑 ∧ ( ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( ( 𝑥 𝐻 𝑦 ) = ∅ ↔ ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) = ∅ ) ∧ 𝑓 : 𝑅 –1-1-onto→ 𝑆 ) ) → ( 1st ‘ ⟨ 𝑓 , ( 𝑧 ∈ 𝑅 , 𝑤 ∈ 𝑅 ↦ ( ( 𝑧 𝐻 𝑤 ) × ( ( 𝑓 ‘ 𝑧 ) 𝐽 ( 𝑓 ‘ 𝑤 ) ) ) ) ⟩ ) : 𝑅 –1-1-onto→ 𝑆 )
48 40 47 jca ⊢ ( ( 𝜑 ∧ ( ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( ( 𝑥 𝐻 𝑦 ) = ∅ ↔ ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) = ∅ ) ∧ 𝑓 : 𝑅 –1-1-onto→ 𝑆 ) ) → ( ⟨ 𝑓 , ( 𝑧 ∈ 𝑅 , 𝑤 ∈ 𝑅 ↦ ( ( 𝑧 𝐻 𝑤 ) × ( ( 𝑓 ‘ 𝑧 ) 𝐽 ( 𝑓 ‘ 𝑤 ) ) ) ) ⟩ ∈ ( ( 𝑋 Full 𝑌 ) ∩ ( 𝑋 Faith 𝑌 ) ) ∧ ( 1st ‘ ⟨ 𝑓 , ( 𝑧 ∈ 𝑅 , 𝑤 ∈ 𝑅 ↦ ( ( 𝑧 𝐻 𝑤 ) × ( ( 𝑓 ‘ 𝑧 ) 𝐽 ( 𝑓 ‘ 𝑤 ) ) ) ) ⟩ ) : 𝑅 –1-1-onto→ 𝑆 ) )
49 1 2 3 4 7 8 9 12 catciso ⊢ ( 𝜑 → ( ⟨ 𝑓 , ( 𝑧 ∈ 𝑅 , 𝑤 ∈ 𝑅 ↦ ( ( 𝑧 𝐻 𝑤 ) × ( ( 𝑓 ‘ 𝑧 ) 𝐽 ( 𝑓 ‘ 𝑤 ) ) ) ) ⟩ ∈ ( 𝑋 ( Iso ‘ 𝐶 ) 𝑌 ) ↔ ( ⟨ 𝑓 , ( 𝑧 ∈ 𝑅 , 𝑤 ∈ 𝑅 ↦ ( ( 𝑧 𝐻 𝑤 ) × ( ( 𝑓 ‘ 𝑧 ) 𝐽 ( 𝑓 ‘ 𝑤 ) ) ) ) ⟩ ∈ ( ( 𝑋 Full 𝑌 ) ∩ ( 𝑋 Faith 𝑌 ) ) ∧ ( 1st ‘ ⟨ 𝑓 , ( 𝑧 ∈ 𝑅 , 𝑤 ∈ 𝑅 ↦ ( ( 𝑧 𝐻 𝑤 ) × ( ( 𝑓 ‘ 𝑧 ) 𝐽 ( 𝑓 ‘ 𝑤 ) ) ) ) ⟩ ) : 𝑅 –1-1-onto→ 𝑆 ) ) )
50 49 biimpar ⊢ ( ( 𝜑 ∧ ( ⟨ 𝑓 , ( 𝑧 ∈ 𝑅 , 𝑤 ∈ 𝑅 ↦ ( ( 𝑧 𝐻 𝑤 ) × ( ( 𝑓 ‘ 𝑧 ) 𝐽 ( 𝑓 ‘ 𝑤 ) ) ) ) ⟩ ∈ ( ( 𝑋 Full 𝑌 ) ∩ ( 𝑋 Faith 𝑌 ) ) ∧ ( 1st ‘ ⟨ 𝑓 , ( 𝑧 ∈ 𝑅 , 𝑤 ∈ 𝑅 ↦ ( ( 𝑧 𝐻 𝑤 ) × ( ( 𝑓 ‘ 𝑧 ) 𝐽 ( 𝑓 ‘ 𝑤 ) ) ) ) ⟩ ) : 𝑅 –1-1-onto→ 𝑆 ) ) → ⟨ 𝑓 , ( 𝑧 ∈ 𝑅 , 𝑤 ∈ 𝑅 ↦ ( ( 𝑧 𝐻 𝑤 ) × ( ( 𝑓 ‘ 𝑧 ) 𝐽 ( 𝑓 ‘ 𝑤 ) ) ) ) ⟩ ∈ ( 𝑋 ( Iso ‘ 𝐶 ) 𝑌 ) )
51 48 50 syldan ⊢ ( ( 𝜑 ∧ ( ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( ( 𝑥 𝐻 𝑦 ) = ∅ ↔ ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) = ∅ ) ∧ 𝑓 : 𝑅 –1-1-onto→ 𝑆 ) ) → ⟨ 𝑓 , ( 𝑧 ∈ 𝑅 , 𝑤 ∈ 𝑅 ↦ ( ( 𝑧 𝐻 𝑤 ) × ( ( 𝑓 ‘ 𝑧 ) 𝐽 ( 𝑓 ‘ 𝑤 ) ) ) ) ⟩ ∈ ( 𝑋 ( Iso ‘ 𝐶 ) 𝑌 ) )
52 eleq1 ⊢ ( 𝑎 = ⟨ 𝑓 , ( 𝑧 ∈ 𝑅 , 𝑤 ∈ 𝑅 ↦ ( ( 𝑧 𝐻 𝑤 ) × ( ( 𝑓 ‘ 𝑧 ) 𝐽 ( 𝑓 ‘ 𝑤 ) ) ) ) ⟩ → ( 𝑎 ∈ ( 𝑋 ( Iso ‘ 𝐶 ) 𝑌 ) ↔ ⟨ 𝑓 , ( 𝑧 ∈ 𝑅 , 𝑤 ∈ 𝑅 ↦ ( ( 𝑧 𝐻 𝑤 ) × ( ( 𝑓 ‘ 𝑧 ) 𝐽 ( 𝑓 ‘ 𝑤 ) ) ) ) ⟩ ∈ ( 𝑋 ( Iso ‘ 𝐶 ) 𝑌 ) ) )
53 17 51 52 spcedv ⊢ ( ( 𝜑 ∧ ( ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( ( 𝑥 𝐻 𝑦 ) = ∅ ↔ ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) = ∅ ) ∧ 𝑓 : 𝑅 –1-1-onto→ 𝑆 ) ) → ∃ 𝑎 𝑎 ∈ ( 𝑋 ( Iso ‘ 𝐶 ) 𝑌 ) )
54 53 ex ⊢ ( 𝜑 → ( ( ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( ( 𝑥 𝐻 𝑦 ) = ∅ ↔ ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) = ∅ ) ∧ 𝑓 : 𝑅 –1-1-onto→ 𝑆 ) → ∃ 𝑎 𝑎 ∈ ( 𝑋 ( Iso ‘ 𝐶 ) 𝑌 ) ) )
55 54 exlimdv ⊢ ( 𝜑 → ( ∃ 𝑓 ( ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( ( 𝑥 𝐻 𝑦 ) = ∅ ↔ ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) = ∅ ) ∧ 𝑓 : 𝑅 –1-1-onto→ 𝑆 ) → ∃ 𝑎 𝑎 ∈ ( 𝑋 ( Iso ‘ 𝐶 ) 𝑌 ) ) )
56 fvexd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝑋 ( Iso ‘ 𝐶 ) 𝑌 ) ) → ( 1st ‘ 𝑎 ) ∈ V )
57 relfull ⊢ Rel ( 𝑋 Full 𝑌 )
58 1 2 3 4 7 8 9 12 catciso ⊢ ( 𝜑 → ( 𝑎 ∈ ( 𝑋 ( Iso ‘ 𝐶 ) 𝑌 ) ↔ ( 𝑎 ∈ ( ( 𝑋 Full 𝑌 ) ∩ ( 𝑋 Faith 𝑌 ) ) ∧ ( 1st ‘ 𝑎 ) : 𝑅 –1-1-onto→ 𝑆 ) ) )
59 58 biimpa ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝑋 ( Iso ‘ 𝐶 ) 𝑌 ) ) → ( 𝑎 ∈ ( ( 𝑋 Full 𝑌 ) ∩ ( 𝑋 Faith 𝑌 ) ) ∧ ( 1st ‘ 𝑎 ) : 𝑅 –1-1-onto→ 𝑆 ) )
60 59 simpld ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝑋 ( Iso ‘ 𝐶 ) 𝑌 ) ) → 𝑎 ∈ ( ( 𝑋 Full 𝑌 ) ∩ ( 𝑋 Faith 𝑌 ) ) )
61 60 elin1d ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝑋 ( Iso ‘ 𝐶 ) 𝑌 ) ) → 𝑎 ∈ ( 𝑋 Full 𝑌 ) )
62 1st2ndbr ⊢ ( ( Rel ( 𝑋 Full 𝑌 ) ∧ 𝑎 ∈ ( 𝑋 Full 𝑌 ) ) → ( 1st ‘ 𝑎 ) ( 𝑋 Full 𝑌 ) ( 2nd ‘ 𝑎 ) )
63 57 61 62 sylancr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝑋 ( Iso ‘ 𝐶 ) 𝑌 ) ) → ( 1st ‘ 𝑎 ) ( 𝑋 Full 𝑌 ) ( 2nd ‘ 𝑎 ) )
64 11 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝑋 ( Iso ‘ 𝐶 ) 𝑌 ) ) → 𝑌 ∈ ThinCat )
65 fullfunc ⊢ ( 𝑋 Full 𝑌 ) ⊆ ( 𝑋 Func 𝑌 )
66 65 ssbri ⊢ ( ( 1st ‘ 𝑎 ) ( 𝑋 Full 𝑌 ) ( 2nd ‘ 𝑎 ) → ( 1st ‘ 𝑎 ) ( 𝑋 Func 𝑌 ) ( 2nd ‘ 𝑎 ) )
67 63 66 syl ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝑋 ( Iso ‘ 𝐶 ) 𝑌 ) ) → ( 1st ‘ 𝑎 ) ( 𝑋 Func 𝑌 ) ( 2nd ‘ 𝑎 ) )
68 3 6 5 64 67 fullthinc ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝑋 ( Iso ‘ 𝐶 ) 𝑌 ) ) → ( ( 1st ‘ 𝑎 ) ( 𝑋 Full 𝑌 ) ( 2nd ‘ 𝑎 ) ↔ ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( ( 𝑥 𝐻 𝑦 ) = ∅ → ( ( ( 1st ‘ 𝑎 ) ‘ 𝑥 ) 𝐽 ( ( 1st ‘ 𝑎 ) ‘ 𝑦 ) ) = ∅ ) ) )
69 63 68 mpbid ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝑋 ( Iso ‘ 𝐶 ) 𝑌 ) ) → ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( ( 𝑥 𝐻 𝑦 ) = ∅ → ( ( ( 1st ‘ 𝑎 ) ‘ 𝑥 ) 𝐽 ( ( 1st ‘ 𝑎 ) ‘ 𝑦 ) ) = ∅ ) )
70 67 adantr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝑋 ( Iso ‘ 𝐶 ) 𝑌 ) ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ) → ( 1st ‘ 𝑎 ) ( 𝑋 Func 𝑌 ) ( 2nd ‘ 𝑎 ) )
71 simprl ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝑋 ( Iso ‘ 𝐶 ) 𝑌 ) ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ) → 𝑥 ∈ 𝑅 )
72 simprr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝑋 ( Iso ‘ 𝐶 ) 𝑌 ) ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ) → 𝑦 ∈ 𝑅 )
73 3 5 6 70 71 72 funcf2 ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝑋 ( Iso ‘ 𝐶 ) 𝑌 ) ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ) → ( 𝑥 ( 2nd ‘ 𝑎 ) 𝑦 ) : ( 𝑥 𝐻 𝑦 ) ⟶ ( ( ( 1st ‘ 𝑎 ) ‘ 𝑥 ) 𝐽 ( ( 1st ‘ 𝑎 ) ‘ 𝑦 ) ) )
74 73 f002 ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝑋 ( Iso ‘ 𝐶 ) 𝑌 ) ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ) → ( ( ( ( 1st ‘ 𝑎 ) ‘ 𝑥 ) 𝐽 ( ( 1st ‘ 𝑎 ) ‘ 𝑦 ) ) = ∅ → ( 𝑥 𝐻 𝑦 ) = ∅ ) )
75 74 ralrimivva ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝑋 ( Iso ‘ 𝐶 ) 𝑌 ) ) → ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( ( ( ( 1st ‘ 𝑎 ) ‘ 𝑥 ) 𝐽 ( ( 1st ‘ 𝑎 ) ‘ 𝑦 ) ) = ∅ → ( 𝑥 𝐻 𝑦 ) = ∅ ) )
76 2ralbiim ⊢ ( ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( ( 𝑥 𝐻 𝑦 ) = ∅ ↔ ( ( ( 1st ‘ 𝑎 ) ‘ 𝑥 ) 𝐽 ( ( 1st ‘ 𝑎 ) ‘ 𝑦 ) ) = ∅ ) ↔ ( ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( ( 𝑥 𝐻 𝑦 ) = ∅ → ( ( ( 1st ‘ 𝑎 ) ‘ 𝑥 ) 𝐽 ( ( 1st ‘ 𝑎 ) ‘ 𝑦 ) ) = ∅ ) ∧ ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( ( ( ( 1st ‘ 𝑎 ) ‘ 𝑥 ) 𝐽 ( ( 1st ‘ 𝑎 ) ‘ 𝑦 ) ) = ∅ → ( 𝑥 𝐻 𝑦 ) = ∅ ) ) )
77 69 75 76 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝑋 ( Iso ‘ 𝐶 ) 𝑌 ) ) → ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( ( 𝑥 𝐻 𝑦 ) = ∅ ↔ ( ( ( 1st ‘ 𝑎 ) ‘ 𝑥 ) 𝐽 ( ( 1st ‘ 𝑎 ) ‘ 𝑦 ) ) = ∅ ) )
78 59 simprd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝑋 ( Iso ‘ 𝐶 ) 𝑌 ) ) → ( 1st ‘ 𝑎 ) : 𝑅 –1-1-onto→ 𝑆 )
79 77 78 jca ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝑋 ( Iso ‘ 𝐶 ) 𝑌 ) ) → ( ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( ( 𝑥 𝐻 𝑦 ) = ∅ ↔ ( ( ( 1st ‘ 𝑎 ) ‘ 𝑥 ) 𝐽 ( ( 1st ‘ 𝑎 ) ‘ 𝑦 ) ) = ∅ ) ∧ ( 1st ‘ 𝑎 ) : 𝑅 –1-1-onto→ 𝑆 ) )
80 fveq1 ⊢ ( 𝑓 = ( 1st ‘ 𝑎 ) → ( 𝑓 ‘ 𝑥 ) = ( ( 1st ‘ 𝑎 ) ‘ 𝑥 ) )
81 fveq1 ⊢ ( 𝑓 = ( 1st ‘ 𝑎 ) → ( 𝑓 ‘ 𝑦 ) = ( ( 1st ‘ 𝑎 ) ‘ 𝑦 ) )
82 80 81 oveq12d ⊢ ( 𝑓 = ( 1st ‘ 𝑎 ) → ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) = ( ( ( 1st ‘ 𝑎 ) ‘ 𝑥 ) 𝐽 ( ( 1st ‘ 𝑎 ) ‘ 𝑦 ) ) )
83 82 eqeq1d ⊢ ( 𝑓 = ( 1st ‘ 𝑎 ) → ( ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) = ∅ ↔ ( ( ( 1st ‘ 𝑎 ) ‘ 𝑥 ) 𝐽 ( ( 1st ‘ 𝑎 ) ‘ 𝑦 ) ) = ∅ ) )
84 83 bibi2d ⊢ ( 𝑓 = ( 1st ‘ 𝑎 ) → ( ( ( 𝑥 𝐻 𝑦 ) = ∅ ↔ ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) = ∅ ) ↔ ( ( 𝑥 𝐻 𝑦 ) = ∅ ↔ ( ( ( 1st ‘ 𝑎 ) ‘ 𝑥 ) 𝐽 ( ( 1st ‘ 𝑎 ) ‘ 𝑦 ) ) = ∅ ) ) )
85 84 2ralbidv ⊢ ( 𝑓 = ( 1st ‘ 𝑎 ) → ( ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( ( 𝑥 𝐻 𝑦 ) = ∅ ↔ ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) = ∅ ) ↔ ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( ( 𝑥 𝐻 𝑦 ) = ∅ ↔ ( ( ( 1st ‘ 𝑎 ) ‘ 𝑥 ) 𝐽 ( ( 1st ‘ 𝑎 ) ‘ 𝑦 ) ) = ∅ ) ) )
86 f1oeq1 ⊢ ( 𝑓 = ( 1st ‘ 𝑎 ) → ( 𝑓 : 𝑅 –1-1-onto→ 𝑆 ↔ ( 1st ‘ 𝑎 ) : 𝑅 –1-1-onto→ 𝑆 ) )
87 85 86 anbi12d ⊢ ( 𝑓 = ( 1st ‘ 𝑎 ) → ( ( ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( ( 𝑥 𝐻 𝑦 ) = ∅ ↔ ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) = ∅ ) ∧ 𝑓 : 𝑅 –1-1-onto→ 𝑆 ) ↔ ( ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( ( 𝑥 𝐻 𝑦 ) = ∅ ↔ ( ( ( 1st ‘ 𝑎 ) ‘ 𝑥 ) 𝐽 ( ( 1st ‘ 𝑎 ) ‘ 𝑦 ) ) = ∅ ) ∧ ( 1st ‘ 𝑎 ) : 𝑅 –1-1-onto→ 𝑆 ) ) )
88 56 79 87 spcedv ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝑋 ( Iso ‘ 𝐶 ) 𝑌 ) ) → ∃ 𝑓 ( ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( ( 𝑥 𝐻 𝑦 ) = ∅ ↔ ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) = ∅ ) ∧ 𝑓 : 𝑅 –1-1-onto→ 𝑆 ) )
89 88 ex ⊢ ( 𝜑 → ( 𝑎 ∈ ( 𝑋 ( Iso ‘ 𝐶 ) 𝑌 ) → ∃ 𝑓 ( ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( ( 𝑥 𝐻 𝑦 ) = ∅ ↔ ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) = ∅ ) ∧ 𝑓 : 𝑅 –1-1-onto→ 𝑆 ) ) )
90 89 exlimdv ⊢ ( 𝜑 → ( ∃ 𝑎 𝑎 ∈ ( 𝑋 ( Iso ‘ 𝐶 ) 𝑌 ) → ∃ 𝑓 ( ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( ( 𝑥 𝐻 𝑦 ) = ∅ ↔ ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) = ∅ ) ∧ 𝑓 : 𝑅 –1-1-onto→ 𝑆 ) ) )
91 55 90 impbid ⊢ ( 𝜑 → ( ∃ 𝑓 ( ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( ( 𝑥 𝐻 𝑦 ) = ∅ ↔ ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) = ∅ ) ∧ 𝑓 : 𝑅 –1-1-onto→ 𝑆 ) ↔ ∃ 𝑎 𝑎 ∈ ( 𝑋 ( Iso ‘ 𝐶 ) 𝑌 ) ) )
92 15 91 bitr4d ⊢ ( 𝜑 → ( 𝑋 ( ≃𝑐 ‘ 𝐶 ) 𝑌 ↔ ∃ 𝑓 ( ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( ( 𝑥 𝐻 𝑦 ) = ∅ ↔ ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) = ∅ ) ∧ 𝑓 : 𝑅 –1-1-onto→ 𝑆 ) ) )