This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝐶 ) = ( 𝑦 ∈ 𝐵 ↦ ∅ ) ) )