Theorem indthincALT

Description: An alternate proof of indthinc assuming more axioms including ax-pow and ax-un . (Contributed by Zhi Wang, 17-Sep-2024) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	indthinc.b	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐶 ) )
	indthinc.h	⊢ ( 𝜑 → ( ( 𝐵 × 𝐵 ) × { 1o } ) = ( Hom ‘ 𝐶 ) )
	indthinc.o	⊢ ( 𝜑 → ∅ = ( comp ‘ 𝐶 ) )
	indthinc.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
Assertion	indthincALT	⊢ ( 𝜑 → ( 𝐶 ∈ ThinCat ∧ ( Id ‘ 𝐶 ) = ( 𝑦 ∈ 𝐵 ↦ ∅ ) ) )

Proof

Step	Hyp	Ref	Expression
1		indthinc.b	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐶 ) )
2		indthinc.h	⊢ ( 𝜑 → ( ( 𝐵 × 𝐵 ) × { 1o } ) = ( Hom ‘ 𝐶 ) )
3		indthinc.o	⊢ ( 𝜑 → ∅ = ( comp ‘ 𝐶 ) )
4		indthinc.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
5		1oex	⊢ 1o ∈ V
6	5	ovconst2	⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ( ( 𝐵 × 𝐵 ) × { 1o } ) 𝑦 ) = 1o )
7		domrefg	⊢ ( 1o ∈ V → 1o ≼ 1o )
8	5 7	ax-mp	⊢ 1o ≼ 1o
9	6 8	eqbrtrdi	⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ( ( 𝐵 × 𝐵 ) × { 1o } ) 𝑦 ) ≼ 1o )
10		modom2	⊢ ( ∃* 𝑓 𝑓 ∈ ( 𝑥 ( ( 𝐵 × 𝐵 ) × { 1o } ) 𝑦 ) ↔ ( 𝑥 ( ( 𝐵 × 𝐵 ) × { 1o } ) 𝑦 ) ≼ 1o )
11	9 10	sylibr	⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ∃* 𝑓 𝑓 ∈ ( 𝑥 ( ( 𝐵 × 𝐵 ) × { 1o } ) 𝑦 ) )
12	11	adantl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ∃* 𝑓 𝑓 ∈ ( 𝑥 ( ( 𝐵 × 𝐵 ) × { 1o } ) 𝑦 ) )
13		biid	⊢ ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 ( ( 𝐵 × 𝐵 ) × { 1o } ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( ( 𝐵 × 𝐵 ) × { 1o } ) 𝑧 ) ) ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 ( ( 𝐵 × 𝐵 ) × { 1o } ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( ( 𝐵 × 𝐵 ) × { 1o } ) 𝑧 ) ) ) )
14		id	⊢ ( 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐵 )
15	14	ancli	⊢ ( 𝑦 ∈ 𝐵 → ( 𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) )
16	5	ovconst2	⊢ ( ( 𝑦 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑦 ( ( 𝐵 × 𝐵 ) × { 1o } ) 𝑦 ) = 1o )
17		0lt1o	⊢ ∅ ∈ 1o
18		eleq2	⊢ ( ( 𝑦 ( ( 𝐵 × 𝐵 ) × { 1o } ) 𝑦 ) = 1o → ( ∅ ∈ ( 𝑦 ( ( 𝐵 × 𝐵 ) × { 1o } ) 𝑦 ) ↔ ∅ ∈ 1o ) )
19	17 18	mpbiri	⊢ ( ( 𝑦 ( ( 𝐵 × 𝐵 ) × { 1o } ) 𝑦 ) = 1o → ∅ ∈ ( 𝑦 ( ( 𝐵 × 𝐵 ) × { 1o } ) 𝑦 ) )
20	15 16 19	3syl	⊢ ( 𝑦 ∈ 𝐵 → ∅ ∈ ( 𝑦 ( ( 𝐵 × 𝐵 ) × { 1o } ) 𝑦 ) )
21	20	adantl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ∅ ∈ ( 𝑦 ( ( 𝐵 × 𝐵 ) × { 1o } ) 𝑦 ) )
22	17	a1i	⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ∅ ∈ 1o )
23		0ov	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∅ 𝑧 ) = ∅
24	23	oveqi	⊢ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ∅ 𝑧 ) 𝑓 ) = ( 𝑔 ∅ 𝑓 )
25		0ov	⊢ ( 𝑔 ∅ 𝑓 ) = ∅
26	24 25	eqtri	⊢ ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ∅ 𝑧 ) 𝑓 ) = ∅
27	26	a1i	⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ∅ 𝑧 ) 𝑓 ) = ∅ )
28	5	ovconst2	⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( 𝑥 ( ( 𝐵 × 𝐵 ) × { 1o } ) 𝑧 ) = 1o )
29	28	3adant2	⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( 𝑥 ( ( 𝐵 × 𝐵 ) × { 1o } ) 𝑧 ) = 1o )
30	22 27 29	3eltr4d	⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ∅ 𝑧 ) 𝑓 ) ∈ ( 𝑥 ( ( 𝐵 × 𝐵 ) × { 1o } ) 𝑧 ) )
31	30	ad2antrl	⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ∧ ( 𝑓 ∈ ( 𝑥 ( ( 𝐵 × 𝐵 ) × { 1o } ) 𝑦 ) ∧ 𝑔 ∈ ( 𝑦 ( ( 𝐵 × 𝐵 ) × { 1o } ) 𝑧 ) ) ) ) → ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ∅ 𝑧 ) 𝑓 ) ∈ ( 𝑥 ( ( 𝐵 × 𝐵 ) × { 1o } ) 𝑧 ) )
32	1 2 12 3 4 13 21 31	isthincd2	⊢ ( 𝜑 → ( 𝐶 ∈ ThinCat ∧ ( Id ‘ 𝐶 ) = ( 𝑦 ∈ 𝐵 ↦ ∅ ) ) )