brttrcl2

Description: Characterization of elements of the transitive closure of a relation. (Contributed by Scott Fenton, 24-Aug-2024)

		Ref	Expression
	Assertion	brttrcl2	Could not format assertion : No typesetting found for \|- ( A t++ R B <-> E. n e. _om E. f ( f Fn suc suc n /\ ( ( f ` (/) ) = A /\ ( f ` suc n ) = B ) /\ A. a e. suc n ( f ` a ) R ( f ` suc a ) ) ) with typecode \|-

Proof

Step	Hyp	Ref	Expression
1		brttrcl	Could not format ( A t++ R B <-> E. m e. ( _om \ 1o ) E. f ( f Fn suc m /\ ( ( f ` (/) ) = A /\ ( f ` m ) = B ) /\ A. a e. m ( f ` a ) R ( f ` suc a ) ) ) : No typesetting found for \|- ( A t++ R B <-> E. m e. ( _om \ 1o ) E. f ( f Fn suc m /\ ( ( f ` (/) ) = A /\ ( f ` m ) = B ) /\ A. a e. m ( f ` a ) R ( f ` suc a ) ) ) with typecode \|-
2		df-1o	$⊢ 1_{𝑜} = suc \emptyset$
3	2	difeq2i	$⊢ ω ∖ 1_{𝑜} = ω ∖ suc \emptyset$
4	3	eleq2i	$⊢ m \in (ω ∖ 1_{𝑜}) \leftrightarrow m \in (ω ∖ suc \emptyset)$
5		peano1	$⊢ \emptyset \in ω$
6		eldifsucnn	$⊢ \emptyset \in ω \to (m \in (ω ∖ suc \emptyset) \leftrightarrow \exists n \in (ω ∖ \emptyset) m = suc n)$
7	5 6	ax-mp	$⊢ m \in (ω ∖ suc \emptyset) \leftrightarrow \exists n \in (ω ∖ \emptyset) m = suc n$
8		dif0	$⊢ ω ∖ \emptyset = ω$
9	8	rexeqi	$⊢ \exists n \in (ω ∖ \emptyset) m = suc n \leftrightarrow \exists n \in ω m = suc n$
10	4 7 9	3bitri	$⊢ m \in (ω ∖ 1_{𝑜}) \leftrightarrow \exists n \in ω m = suc n$
11	10	anbi1i	$⊢ (m \in (ω ∖ 1_{𝑜}) \land \exists f (f Fn suc m \land (f (\emptyset) = A \land f (m) = B) \land \forall a \in m f (a) R f (suc a))) \leftrightarrow (\exists n \in ω m = suc n \land \exists f (f Fn suc m \land (f (\emptyset) = A \land f (m) = B) \land \forall a \in m f (a) R f (suc a)))$
12		r19.41v	$⊢ \exists n \in ω (m = suc n \land \exists f (f Fn suc m \land (f (\emptyset) = A \land f (m) = B) \land \forall a \in m f (a) R f (suc a))) \leftrightarrow (\exists n \in ω m = suc n \land \exists f (f Fn suc m \land (f (\emptyset) = A \land f (m) = B) \land \forall a \in m f (a) R f (suc a)))$
13	11 12	bitr4i	$⊢ (m \in (ω ∖ 1_{𝑜}) \land \exists f (f Fn suc m \land (f (\emptyset) = A \land f (m) = B) \land \forall a \in m f (a) R f (suc a))) \leftrightarrow \exists n \in ω (m = suc n \land \exists f (f Fn suc m \land (f (\emptyset) = A \land f (m) = B) \land \forall a \in m f (a) R f (suc a)))$
14	13	exbii	$⊢ \exists m (m \in (ω ∖ 1_{𝑜}) \land \exists f (f Fn suc m \land (f (\emptyset) = A \land f (m) = B) \land \forall a \in m f (a) R f (suc a))) \leftrightarrow \exists m \exists n \in ω (m = suc n \land \exists f (f Fn suc m \land (f (\emptyset) = A \land f (m) = B) \land \forall a \in m f (a) R f (suc a)))$
15		df-rex	$⊢ \exists m \in (ω ∖ 1_{𝑜}) \exists f (f Fn suc m \land (f (\emptyset) = A \land f (m) = B) \land \forall a \in m f (a) R f (suc a)) \leftrightarrow \exists m (m \in (ω ∖ 1_{𝑜}) \land \exists f (f Fn suc m \land (f (\emptyset) = A \land f (m) = B) \land \forall a \in m f (a) R f (suc a)))$
16		rexcom4	$⊢ \exists n \in ω \exists m (m = suc n \land \exists f (f Fn suc m \land (f (\emptyset) = A \land f (m) = B) \land \forall a \in m f (a) R f (suc a))) \leftrightarrow \exists m \exists n \in ω (m = suc n \land \exists f (f Fn suc m \land (f (\emptyset) = A \land f (m) = B) \land \forall a \in m f (a) R f (suc a)))$
17	14 15 16	3bitr4i	$⊢ \exists m \in (ω ∖ 1_{𝑜}) \exists f (f Fn suc m \land (f (\emptyset) = A \land f (m) = B) \land \forall a \in m f (a) R f (suc a)) \leftrightarrow \exists n \in ω \exists m (m = suc n \land \exists f (f Fn suc m \land (f (\emptyset) = A \land f (m) = B) \land \forall a \in m f (a) R f (suc a)))$
18		vex	$⊢ n \in V$
19	18	sucex	$⊢ suc n \in V$
20		suceq	$⊢ m = suc n \to suc m = suc suc n$
21	20	fneq2d	$⊢ m = suc n \to (f Fn suc m \leftrightarrow f Fn suc suc n)$
22		fveqeq2	$⊢ m = suc n \to (f (m) = B \leftrightarrow f (suc n) = B)$
23	22	anbi2d	$⊢ m = suc n \to ((f (\emptyset) = A \land f (m) = B) \leftrightarrow (f (\emptyset) = A \land f (suc n) = B))$
24		raleq	$⊢ m = suc n \to (\forall a \in m f (a) R f (suc a) \leftrightarrow \forall a \in suc n f (a) R f (suc a))$
25	21 23 24	3anbi123d	$⊢ m = suc n \to ((f Fn suc m \land (f (\emptyset) = A \land f (m) = B) \land \forall a \in m f (a) R f (suc a)) \leftrightarrow (f Fn suc suc n \land (f (\emptyset) = A \land f (suc n) = B) \land \forall a \in suc n f (a) R f (suc a)))$
26	25	exbidv	$⊢ m = suc n \to (\exists f (f Fn suc m \land (f (\emptyset) = A \land f (m) = B) \land \forall a \in m f (a) R f (suc a)) \leftrightarrow \exists f (f Fn suc suc n \land (f (\emptyset) = A \land f (suc n) = B) \land \forall a \in suc n f (a) R f (suc a)))$
27	19 26	ceqsexv	$⊢ \exists m (m = suc n \land \exists f (f Fn suc m \land (f (\emptyset) = A \land f (m) = B) \land \forall a \in m f (a) R f (suc a))) \leftrightarrow \exists f (f Fn suc suc n \land (f (\emptyset) = A \land f (suc n) = B) \land \forall a \in suc n f (a) R f (suc a))$
28	27	rexbii	$⊢ \exists n \in ω \exists m (m = suc n \land \exists f (f Fn suc m \land (f (\emptyset) = A \land f (m) = B) \land \forall a \in m f (a) R f (suc a))) \leftrightarrow \exists n \in ω \exists f (f Fn suc suc n \land (f (\emptyset) = A \land f (suc n) = B) \land \forall a \in suc n f (a) R f (suc a))$
29	1 17 28	3bitri	Could not format ( A t++ R B <-> E. n e. _om E. f ( f Fn suc suc n /\ ( ( f ` (/) ) = A /\ ( f ` suc n ) = B ) /\ A. a e. suc n ( f ` a ) R ( f ` suc a ) ) ) : No typesetting found for \|- ( A t++ R B <-> E. n e. _om E. f ( f Fn suc suc n /\ ( ( f ` (/) ) = A /\ ( f ` suc n ) = B ) /\ A. a e. suc n ( f ` a ) R ( f ` suc a ) ) ) with typecode \|-

Metamath Proof Explorer

Theorem brttrcl2

Proof