indthincALT

Description: An alternate proof for 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	$⊢ φ \to B = {Base}_{C}$
	indthinc.h	$⊢ φ \to (B \times B) \times \{1_{𝑜}\} = Hom (C)$
	indthinc.o	$⊢ φ \to \emptyset = comp (C)$
	indthinc.c	$⊢ φ \to C \in V$
Assertion	indthincALT	Could not format assertion : No typesetting found for \|- ( ph -> ( C e. ThinCat /\ ( Id ` C ) = ( y e. B \|-> (/) ) ) ) with typecode \|-

Proof

Step	Hyp	Ref	Expression
1		indthinc.b	$⊢ φ \to B = {Base}_{C}$
2		indthinc.h	$⊢ φ \to (B \times B) \times \{1_{𝑜}\} = Hom (C)$
3		indthinc.o	$⊢ φ \to \emptyset = comp (C)$
4		indthinc.c	$⊢ φ \to C \in V$
5		1oex	$⊢ 1_{𝑜} \in V$
6	5	ovconst2	$⊢ (x \in B \land y \in B) \to x ((B \times B) \times \{1_{𝑜}\}) y = 1_{𝑜}$
7		domrefg	$⊢ 1_{𝑜} \in V \to 1_{𝑜} ≼ 1_{𝑜}$
8	5 7	ax-mp	$⊢ 1_{𝑜} ≼ 1_{𝑜}$
9	6 8	eqbrtrdi	$⊢ (x \in B \land y \in B) \to (x ((B \times B) \times \{1_{𝑜}\}) y) ≼ 1_{𝑜}$
10		modom2	$⊢ \exists^{*} f f \in (x ((B \times B) \times \{1_{𝑜}\}) y) \leftrightarrow (x ((B \times B) \times \{1_{𝑜}\}) y) ≼ 1_{𝑜}$
11	9 10	sylibr	$⊢ (x \in B \land y \in B) \to \exists^{*} f f \in (x ((B \times B) \times \{1_{𝑜}\}) y)$
12	11	adantl	$⊢ (φ \land (x \in B \land y \in B)) \to \exists^{*} f f \in (x ((B \times B) \times \{1_{𝑜}\}) y)$
13		biid	$⊢ ((x \in B \land y \in B \land z \in B) \land (f \in (x ((B \times B) \times \{1_{𝑜}\}) y) \land g \in (y ((B \times B) \times \{1_{𝑜}\}) z))) \leftrightarrow ((x \in B \land y \in B \land z \in B) \land (f \in (x ((B \times B) \times \{1_{𝑜}\}) y) \land g \in (y ((B \times B) \times \{1_{𝑜}\}) z)))$
14		id	$⊢ y \in B \to y \in B$
15	14	ancli	$⊢ y \in B \to (y \in B \land y \in B)$
16	5	ovconst2	$⊢ (y \in B \land y \in B) \to y ((B \times B) \times \{1_{𝑜}\}) y = 1_{𝑜}$
17		0lt1o	$⊢ \emptyset \in 1_{𝑜}$
18		eleq2	$⊢ y ((B \times B) \times \{1_{𝑜}\}) y = 1_{𝑜} \to (\emptyset \in (y ((B \times B) \times \{1_{𝑜}\}) y) \leftrightarrow \emptyset \in 1_{𝑜})$
19	17 18	mpbiri	$⊢ y ((B \times B) \times \{1_{𝑜}\}) y = 1_{𝑜} \to \emptyset \in (y ((B \times B) \times \{1_{𝑜}\}) y)$
20	15 16 19	3syl	$⊢ y \in B \to \emptyset \in (y ((B \times B) \times \{1_{𝑜}\}) y)$
21	20	adantl	$⊢ (φ \land y \in B) \to \emptyset \in (y ((B \times B) \times \{1_{𝑜}\}) y)$
22	17	a1i	$⊢ (x \in B \land y \in B \land z \in B) \to \emptyset \in 1_{𝑜}$
23		0ov	$⊢ ⟨x, y⟩ \emptyset z = \emptyset$
24	23	oveqi	$⊢ g (⟨x, y⟩ \emptyset z) f = g \emptyset f$
25		0ov	$⊢ g \emptyset f = \emptyset$
26	24 25	eqtri	$⊢ g (⟨x, y⟩ \emptyset z) f = \emptyset$
27	26	a1i	$⊢ (x \in B \land y \in B \land z \in B) \to g (⟨x, y⟩ \emptyset z) f = \emptyset$
28	5	ovconst2	$⊢ (x \in B \land z \in B) \to x ((B \times B) \times \{1_{𝑜}\}) z = 1_{𝑜}$
29	28	3adant2	$⊢ (x \in B \land y \in B \land z \in B) \to x ((B \times B) \times \{1_{𝑜}\}) z = 1_{𝑜}$
30	22 27 29	3eltr4d	$⊢ (x \in B \land y \in B \land z \in B) \to g (⟨x, y⟩ \emptyset z) f \in (x ((B \times B) \times \{1_{𝑜}\}) z)$
31	30	ad2antrl	$⊢ (φ \land ((x \in B \land y \in B \land z \in B) \land (f \in (x ((B \times B) \times \{1_{𝑜}\}) y) \land g \in (y ((B \times B) \times \{1_{𝑜}\}) z)))) \to g (⟨x, y⟩ \emptyset z) f \in (x ((B \times B) \times \{1_{𝑜}\}) z)$
32	1 2 12 3 4 13 21 31	isthincd2	Could not format ( ph -> ( C e. ThinCat /\ ( Id ` C ) = ( y e. B \|-> (/) ) ) ) : No typesetting found for \|- ( ph -> ( C e. ThinCat /\ ( Id ` C ) = ( y e. B \|-> (/) ) ) ) with typecode \|-

Metamath Proof Explorer

Theorem indthincALT

Proof