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	thinccd	⊢ ( ( 𝜑 ∧ ( ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( ( 𝑥 𝐻 𝑦 ) = ∅ ↔ ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) = ∅ ) ∧ 𝑓 : 𝑅 –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	⊢ ( 1^st ‘ ⟨ 𝑓 , ( 𝑧 ∈ 𝑅 , 𝑤 ∈ 𝑅 ↦ ( ( 𝑧 𝐻 𝑤 ) × ( ( 𝑓 ‘ 𝑧 ) 𝐽 ( 𝑓 ‘ 𝑤 ) ) ) ) ⟩ ) = 𝑓
45		f1oeq1	⊢ ( ( 1^st ‘ ⟨ 𝑓 , ( 𝑧 ∈ 𝑅 , 𝑤 ∈ 𝑅 ↦ ( ( 𝑧 𝐻 𝑤 ) × ( ( 𝑓 ‘ 𝑧 ) 𝐽 ( 𝑓 ‘ 𝑤 ) ) ) ) ⟩ ) = 𝑓 → ( ( 1^st ‘ ⟨ 𝑓 , ( 𝑧 ∈ 𝑅 , 𝑤 ∈ 𝑅 ↦ ( ( 𝑧 𝐻 𝑤 ) × ( ( 𝑓 ‘ 𝑧 ) 𝐽 ( 𝑓 ‘ 𝑤 ) ) ) ) ⟩ ) : 𝑅 –1-1-onto→ 𝑆 ↔ 𝑓 : 𝑅 –1-1-onto→ 𝑆 ) )
46	44 45	ax-mp	⊢ ( ( 1^st ‘ ⟨ 𝑓 , ( 𝑧 ∈ 𝑅 , 𝑤 ∈ 𝑅 ↦ ( ( 𝑧 𝐻 𝑤 ) × ( ( 𝑓 ‘ 𝑧 ) 𝐽 ( 𝑓 ‘ 𝑤 ) ) ) ) ⟩ ) : 𝑅 –1-1-onto→ 𝑆 ↔ 𝑓 : 𝑅 –1-1-onto→ 𝑆 )
47	25 46	sylibr	⊢ ( ( 𝜑 ∧ ( ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( ( 𝑥 𝐻 𝑦 ) = ∅ ↔ ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) = ∅ ) ∧ 𝑓 : 𝑅 –1-1-onto→ 𝑆 ) ) → ( 1^st ‘ ⟨ 𝑓 , ( 𝑧 ∈ 𝑅 , 𝑤 ∈ 𝑅 ↦ ( ( 𝑧 𝐻 𝑤 ) × ( ( 𝑓 ‘ 𝑧 ) 𝐽 ( 𝑓 ‘ 𝑤 ) ) ) ) ⟩ ) : 𝑅 –1-1-onto→ 𝑆 )
48	40 47	jca	⊢ ( ( 𝜑 ∧ ( ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( ( 𝑥 𝐻 𝑦 ) = ∅ ↔ ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) = ∅ ) ∧ 𝑓 : 𝑅 –1-1-onto→ 𝑆 ) ) → ( ⟨ 𝑓 , ( 𝑧 ∈ 𝑅 , 𝑤 ∈ 𝑅 ↦ ( ( 𝑧 𝐻 𝑤 ) × ( ( 𝑓 ‘ 𝑧 ) 𝐽 ( 𝑓 ‘ 𝑤 ) ) ) ) ⟩ ∈ ( ( 𝑋 Full 𝑌 ) ∩ ( 𝑋 Faith 𝑌 ) ) ∧ ( 1^st ‘ ⟨ 𝑓 , ( 𝑧 ∈ 𝑅 , 𝑤 ∈ 𝑅 ↦ ( ( 𝑧 𝐻 𝑤 ) × ( ( 𝑓 ‘ 𝑧 ) 𝐽 ( 𝑓 ‘ 𝑤 ) ) ) ) ⟩ ) : 𝑅 –1-1-onto→ 𝑆 ) )
49	1 2 3 4 7 8 9 12	catciso	⊢ ( 𝜑 → ( ⟨ 𝑓 , ( 𝑧 ∈ 𝑅 , 𝑤 ∈ 𝑅 ↦ ( ( 𝑧 𝐻 𝑤 ) × ( ( 𝑓 ‘ 𝑧 ) 𝐽 ( 𝑓 ‘ 𝑤 ) ) ) ) ⟩ ∈ ( 𝑋 ( Iso ‘ 𝐶 ) 𝑌 ) ↔ ( ⟨ 𝑓 , ( 𝑧 ∈ 𝑅 , 𝑤 ∈ 𝑅 ↦ ( ( 𝑧 𝐻 𝑤 ) × ( ( 𝑓 ‘ 𝑧 ) 𝐽 ( 𝑓 ‘ 𝑤 ) ) ) ) ⟩ ∈ ( ( 𝑋 Full 𝑌 ) ∩ ( 𝑋 Faith 𝑌 ) ) ∧ ( 1^st ‘ ⟨ 𝑓 , ( 𝑧 ∈ 𝑅 , 𝑤 ∈ 𝑅 ↦ ( ( 𝑧 𝐻 𝑤 ) × ( ( 𝑓 ‘ 𝑧 ) 𝐽 ( 𝑓 ‘ 𝑤 ) ) ) ) ⟩ ) : 𝑅 –1-1-onto→ 𝑆 ) ) )
50	49	biimpar	⊢ ( ( 𝜑 ∧ ( ⟨ 𝑓 , ( 𝑧 ∈ 𝑅 , 𝑤 ∈ 𝑅 ↦ ( ( 𝑧 𝐻 𝑤 ) × ( ( 𝑓 ‘ 𝑧 ) 𝐽 ( 𝑓 ‘ 𝑤 ) ) ) ) ⟩ ∈ ( ( 𝑋 Full 𝑌 ) ∩ ( 𝑋 Faith 𝑌 ) ) ∧ ( 1^st ‘ ⟨ 𝑓 , ( 𝑧 ∈ 𝑅 , 𝑤 ∈ 𝑅 ↦ ( ( 𝑧 𝐻 𝑤 ) × ( ( 𝑓 ‘ 𝑧 ) 𝐽 ( 𝑓 ‘ 𝑤 ) ) ) ) ⟩ ) : 𝑅 –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 ‘ 𝐶 ) 𝑌 ) ) → ( 1^st ‘ 𝑎 ) ∈ V )
57		relfull	⊢ Rel ( 𝑋 Full 𝑌 )
58	1 2 3 4 7 8 9 12	catciso	⊢ ( 𝜑 → ( 𝑎 ∈ ( 𝑋 ( Iso ‘ 𝐶 ) 𝑌 ) ↔ ( 𝑎 ∈ ( ( 𝑋 Full 𝑌 ) ∩ ( 𝑋 Faith 𝑌 ) ) ∧ ( 1^st ‘ 𝑎 ) : 𝑅 –1-1-onto→ 𝑆 ) ) )
59	58	biimpa	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝑋 ( Iso ‘ 𝐶 ) 𝑌 ) ) → ( 𝑎 ∈ ( ( 𝑋 Full 𝑌 ) ∩ ( 𝑋 Faith 𝑌 ) ) ∧ ( 1^st ‘ 𝑎 ) : 𝑅 –1-1-onto→ 𝑆 ) )
60	59	simpld	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝑋 ( Iso ‘ 𝐶 ) 𝑌 ) ) → 𝑎 ∈ ( ( 𝑋 Full 𝑌 ) ∩ ( 𝑋 Faith 𝑌 ) ) )
61	60	elin1d	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝑋 ( Iso ‘ 𝐶 ) 𝑌 ) ) → 𝑎 ∈ ( 𝑋 Full 𝑌 ) )
62		1st2ndbr	⊢ ( ( Rel ( 𝑋 Full 𝑌 ) ∧ 𝑎 ∈ ( 𝑋 Full 𝑌 ) ) → ( 1^st ‘ 𝑎 ) ( 𝑋 Full 𝑌 ) ( 2^nd ‘ 𝑎 ) )
63	57 61 62	sylancr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝑋 ( Iso ‘ 𝐶 ) 𝑌 ) ) → ( 1^st ‘ 𝑎 ) ( 𝑋 Full 𝑌 ) ( 2^nd ‘ 𝑎 ) )
64	11	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝑋 ( Iso ‘ 𝐶 ) 𝑌 ) ) → 𝑌 ∈ ThinCat )
65		fullfunc	⊢ ( 𝑋 Full 𝑌 ) ⊆ ( 𝑋 Func 𝑌 )
66	65	ssbri	⊢ ( ( 1^st ‘ 𝑎 ) ( 𝑋 Full 𝑌 ) ( 2^nd ‘ 𝑎 ) → ( 1^st ‘ 𝑎 ) ( 𝑋 Func 𝑌 ) ( 2^nd ‘ 𝑎 ) )
67	63 66	syl	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝑋 ( Iso ‘ 𝐶 ) 𝑌 ) ) → ( 1^st ‘ 𝑎 ) ( 𝑋 Func 𝑌 ) ( 2^nd ‘ 𝑎 ) )
68	3 6 5 64 67	fullthinc	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝑋 ( Iso ‘ 𝐶 ) 𝑌 ) ) → ( ( 1^st ‘ 𝑎 ) ( 𝑋 Full 𝑌 ) ( 2^nd ‘ 𝑎 ) ↔ ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( ( 𝑥 𝐻 𝑦 ) = ∅ → ( ( ( 1^st ‘ 𝑎 ) ‘ 𝑥 ) 𝐽 ( ( 1^st ‘ 𝑎 ) ‘ 𝑦 ) ) = ∅ ) ) )
69	63 68	mpbid	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝑋 ( Iso ‘ 𝐶 ) 𝑌 ) ) → ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( ( 𝑥 𝐻 𝑦 ) = ∅ → ( ( ( 1^st ‘ 𝑎 ) ‘ 𝑥 ) 𝐽 ( ( 1^st ‘ 𝑎 ) ‘ 𝑦 ) ) = ∅ ) )
70	67	adantr	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝑋 ( Iso ‘ 𝐶 ) 𝑌 ) ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ) → ( 1^st ‘ 𝑎 ) ( 𝑋 Func 𝑌 ) ( 2^nd ‘ 𝑎 ) )
71		simprl	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝑋 ( Iso ‘ 𝐶 ) 𝑌 ) ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ) → 𝑥 ∈ 𝑅 )
72		simprr	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝑋 ( Iso ‘ 𝐶 ) 𝑌 ) ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ) → 𝑦 ∈ 𝑅 )
73	3 5 6 70 71 72	funcf2	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝑋 ( Iso ‘ 𝐶 ) 𝑌 ) ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ) → ( 𝑥 ( 2^nd ‘ 𝑎 ) 𝑦 ) : ( 𝑥 𝐻 𝑦 ) ⟶ ( ( ( 1^st ‘ 𝑎 ) ‘ 𝑥 ) 𝐽 ( ( 1^st ‘ 𝑎 ) ‘ 𝑦 ) ) )
74	73	f002	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝑋 ( Iso ‘ 𝐶 ) 𝑌 ) ) ∧ ( 𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅 ) ) → ( ( ( ( 1^st ‘ 𝑎 ) ‘ 𝑥 ) 𝐽 ( ( 1^st ‘ 𝑎 ) ‘ 𝑦 ) ) = ∅ → ( 𝑥 𝐻 𝑦 ) = ∅ ) )
75	74	ralrimivva	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝑋 ( Iso ‘ 𝐶 ) 𝑌 ) ) → ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( ( ( ( 1^st ‘ 𝑎 ) ‘ 𝑥 ) 𝐽 ( ( 1^st ‘ 𝑎 ) ‘ 𝑦 ) ) = ∅ → ( 𝑥 𝐻 𝑦 ) = ∅ ) )
76		2ralbiim	⊢ ( ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( ( 𝑥 𝐻 𝑦 ) = ∅ ↔ ( ( ( 1^st ‘ 𝑎 ) ‘ 𝑥 ) 𝐽 ( ( 1^st ‘ 𝑎 ) ‘ 𝑦 ) ) = ∅ ) ↔ ( ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( ( 𝑥 𝐻 𝑦 ) = ∅ → ( ( ( 1^st ‘ 𝑎 ) ‘ 𝑥 ) 𝐽 ( ( 1^st ‘ 𝑎 ) ‘ 𝑦 ) ) = ∅ ) ∧ ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( ( ( ( 1^st ‘ 𝑎 ) ‘ 𝑥 ) 𝐽 ( ( 1^st ‘ 𝑎 ) ‘ 𝑦 ) ) = ∅ → ( 𝑥 𝐻 𝑦 ) = ∅ ) ) )
77	69 75 76	sylanbrc	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝑋 ( Iso ‘ 𝐶 ) 𝑌 ) ) → ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( ( 𝑥 𝐻 𝑦 ) = ∅ ↔ ( ( ( 1^st ‘ 𝑎 ) ‘ 𝑥 ) 𝐽 ( ( 1^st ‘ 𝑎 ) ‘ 𝑦 ) ) = ∅ ) )
78	59	simprd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝑋 ( Iso ‘ 𝐶 ) 𝑌 ) ) → ( 1^st ‘ 𝑎 ) : 𝑅 –1-1-onto→ 𝑆 )
79	77 78	jca	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝑋 ( Iso ‘ 𝐶 ) 𝑌 ) ) → ( ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( ( 𝑥 𝐻 𝑦 ) = ∅ ↔ ( ( ( 1^st ‘ 𝑎 ) ‘ 𝑥 ) 𝐽 ( ( 1^st ‘ 𝑎 ) ‘ 𝑦 ) ) = ∅ ) ∧ ( 1^st ‘ 𝑎 ) : 𝑅 –1-1-onto→ 𝑆 ) )
80		fveq1	⊢ ( 𝑓 = ( 1^st ‘ 𝑎 ) → ( 𝑓 ‘ 𝑥 ) = ( ( 1^st ‘ 𝑎 ) ‘ 𝑥 ) )
81		fveq1	⊢ ( 𝑓 = ( 1^st ‘ 𝑎 ) → ( 𝑓 ‘ 𝑦 ) = ( ( 1^st ‘ 𝑎 ) ‘ 𝑦 ) )
82	80 81	oveq12d	⊢ ( 𝑓 = ( 1^st ‘ 𝑎 ) → ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) = ( ( ( 1^st ‘ 𝑎 ) ‘ 𝑥 ) 𝐽 ( ( 1^st ‘ 𝑎 ) ‘ 𝑦 ) ) )
83	82	eqeq1d	⊢ ( 𝑓 = ( 1^st ‘ 𝑎 ) → ( ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) = ∅ ↔ ( ( ( 1^st ‘ 𝑎 ) ‘ 𝑥 ) 𝐽 ( ( 1^st ‘ 𝑎 ) ‘ 𝑦 ) ) = ∅ ) )
84	83	bibi2d	⊢ ( 𝑓 = ( 1^st ‘ 𝑎 ) → ( ( ( 𝑥 𝐻 𝑦 ) = ∅ ↔ ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) = ∅ ) ↔ ( ( 𝑥 𝐻 𝑦 ) = ∅ ↔ ( ( ( 1^st ‘ 𝑎 ) ‘ 𝑥 ) 𝐽 ( ( 1^st ‘ 𝑎 ) ‘ 𝑦 ) ) = ∅ ) ) )
85	84	2ralbidv	⊢ ( 𝑓 = ( 1^st ‘ 𝑎 ) → ( ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( ( 𝑥 𝐻 𝑦 ) = ∅ ↔ ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) = ∅ ) ↔ ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( ( 𝑥 𝐻 𝑦 ) = ∅ ↔ ( ( ( 1^st ‘ 𝑎 ) ‘ 𝑥 ) 𝐽 ( ( 1^st ‘ 𝑎 ) ‘ 𝑦 ) ) = ∅ ) ) )
86		f1oeq1	⊢ ( 𝑓 = ( 1^st ‘ 𝑎 ) → ( 𝑓 : 𝑅 –1-1-onto→ 𝑆 ↔ ( 1^st ‘ 𝑎 ) : 𝑅 –1-1-onto→ 𝑆 ) )
87	85 86	anbi12d	⊢ ( 𝑓 = ( 1^st ‘ 𝑎 ) → ( ( ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( ( 𝑥 𝐻 𝑦 ) = ∅ ↔ ( ( 𝑓 ‘ 𝑥 ) 𝐽 ( 𝑓 ‘ 𝑦 ) ) = ∅ ) ∧ 𝑓 : 𝑅 –1-1-onto→ 𝑆 ) ↔ ( ∀ 𝑥 ∈ 𝑅 ∀ 𝑦 ∈ 𝑅 ( ( 𝑥 𝐻 𝑦 ) = ∅ ↔ ( ( ( 1^st ‘ 𝑎 ) ‘ 𝑥 ) 𝐽 ( ( 1^st ‘ 𝑎 ) ‘ 𝑦 ) ) = ∅ ) ∧ ( 1^st ‘ 𝑎 ) : 𝑅 –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→ 𝑆 ) ) )

Metamath Proof Explorer

Theorem thincciso

Proof