ttrclse

Description: If R is set-like over A , then the transitive closure of the restriction of R to A is set-like over A .

This theorem requires the axioms of infinity and replacement for its proof. (Contributed by Scott Fenton, 31-Oct-2024)

		Ref	Expression
	Assertion	ttrclse	$⊢ R Se A \to t++ ({R ↾}_{A}) Se A$

Proof

Step	Hyp	Ref	Expression
1		brttrcl2	$⊢ y t++ ({R ↾}_{A}) x \leftrightarrow \exists n \in ω \exists f (f Fn suc suc n \land (f (\emptyset) = y \land f (suc n) = x) \land \forall a \in suc n f (a) ({R ↾}_{A}) f (suc a))$
2		eqid	$⊢ rec ((b \in V ⟼ ⋃_{w \in b} Pred (R, A, w)), Pred (R, A, x)) = rec ((b \in V ⟼ ⋃_{w \in b} Pred (R, A, w)), Pred (R, A, x))$
3	2	ttrclselem2	$⊢ (n \in ω \land R Se A \land x \in A) \to (\exists f (f Fn suc suc n \land (f (\emptyset) = y \land f (suc n) = x) \land \forall a \in suc n f (a) ({R ↾}_{A}) f (suc a)) \leftrightarrow y \in rec ((b \in V ⟼ ⋃_{w \in b} Pred (R, A, w)), Pred (R, A, x)) (n))$
4	3	3expb	$⊢ (n \in ω \land (R Se A \land x \in A)) \to (\exists f (f Fn suc suc n \land (f (\emptyset) = y \land f (suc n) = x) \land \forall a \in suc n f (a) ({R ↾}_{A}) f (suc a)) \leftrightarrow y \in rec ((b \in V ⟼ ⋃_{w \in b} Pred (R, A, w)), Pred (R, A, x)) (n))$
5	4	ancoms	$⊢ ((R Se A \land x \in A) \land n \in ω) \to (\exists f (f Fn suc suc n \land (f (\emptyset) = y \land f (suc n) = x) \land \forall a \in suc n f (a) ({R ↾}_{A}) f (suc a)) \leftrightarrow y \in rec ((b \in V ⟼ ⋃_{w \in b} Pred (R, A, w)), Pred (R, A, x)) (n))$
6	5	rexbidva	$⊢ (R Se A \land x \in A) \to (\exists n \in ω \exists f (f Fn suc suc n \land (f (\emptyset) = y \land f (suc n) = x) \land \forall a \in suc n f (a) ({R ↾}_{A}) f (suc a)) \leftrightarrow \exists n \in ω y \in rec ((b \in V ⟼ ⋃_{w \in b} Pred (R, A, w)), Pred (R, A, x)) (n))$
7	1 6	bitrid	$⊢ (R Se A \land x \in A) \to (y t++ ({R ↾}_{A}) x \leftrightarrow \exists n \in ω y \in rec ((b \in V ⟼ ⋃_{w \in b} Pred (R, A, w)), Pred (R, A, x)) (n))$
8		vex	$⊢ y \in V$
9	8	elpred	$⊢ x \in V \to (y \in Pred (t++ ({R ↾}_{A}), A, x) \leftrightarrow (y \in A \land y t++ ({R ↾}_{A}) x))$
10	9	elv	$⊢ y \in Pred (t++ ({R ↾}_{A}), A, x) \leftrightarrow (y \in A \land y t++ ({R ↾}_{A}) x)$
11		resdmss	$⊢ dom ({R ↾}_{A}) \subseteq A$
12		vex	$⊢ x \in V$
13	8 12	breldm	$⊢ y t++ ({R ↾}_{A}) x \to y \in dom t++ ({R ↾}_{A})$
14		dmttrcl	$⊢ dom t++ ({R ↾}_{A}) = dom ({R ↾}_{A})$
15	13 14	eleqtrdi	$⊢ y t++ ({R ↾}_{A}) x \to y \in dom ({R ↾}_{A})$
16	11 15	sselid	$⊢ y t++ ({R ↾}_{A}) x \to y \in A$
17	16	pm4.71ri	$⊢ y t++ ({R ↾}_{A}) x \leftrightarrow (y \in A \land y t++ ({R ↾}_{A}) x)$
18	10 17	bitr4i	$⊢ y \in Pred (t++ ({R ↾}_{A}), A, x) \leftrightarrow y t++ ({R ↾}_{A}) x$
19		rdgfun	$⊢ Fun rec ((b \in V ⟼ ⋃_{w \in b} Pred (R, A, w)), Pred (R, A, x))$
20		eluniima	$⊢ Fun rec ((b \in V ⟼ ⋃_{w \in b} Pred (R, A, w)), Pred (R, A, x)) \to (y \in ⋃ rec ((b \in V ⟼ ⋃_{w \in b} Pred (R, A, w)), Pred (R, A, x)) [ω] \leftrightarrow \exists n \in ω y \in rec ((b \in V ⟼ ⋃_{w \in b} Pred (R, A, w)), Pred (R, A, x)) (n))$
21	19 20	ax-mp	$⊢ y \in ⋃ rec ((b \in V ⟼ ⋃_{w \in b} Pred (R, A, w)), Pred (R, A, x)) [ω] \leftrightarrow \exists n \in ω y \in rec ((b \in V ⟼ ⋃_{w \in b} Pred (R, A, w)), Pred (R, A, x)) (n)$
22	7 18 21	3bitr4g	$⊢ (R Se A \land x \in A) \to (y \in Pred (t++ ({R ↾}_{A}), A, x) \leftrightarrow y \in ⋃ rec ((b \in V ⟼ ⋃_{w \in b} Pred (R, A, w)), Pred (R, A, x)) [ω])$
23	22	eqrdv	$⊢ (R Se A \land x \in A) \to Pred (t++ ({R ↾}_{A}), A, x) = ⋃ rec ((b \in V ⟼ ⋃_{w \in b} Pred (R, A, w)), Pred (R, A, x)) [ω]$
24		omex	$⊢ ω \in V$
25	24	funimaex	$⊢ Fun rec ((b \in V ⟼ ⋃_{w \in b} Pred (R, A, w)), Pred (R, A, x)) \to rec ((b \in V ⟼ ⋃_{w \in b} Pred (R, A, w)), Pred (R, A, x)) [ω] \in V$
26	19 25	ax-mp	$⊢ rec ((b \in V ⟼ ⋃_{w \in b} Pred (R, A, w)), Pred (R, A, x)) [ω] \in V$
27	26	uniex	$⊢ ⋃ rec ((b \in V ⟼ ⋃_{w \in b} Pred (R, A, w)), Pred (R, A, x)) [ω] \in V$
28	23 27	eqeltrdi	$⊢ (R Se A \land x \in A) \to Pred (t++ ({R ↾}_{A}), A, x) \in V$
29	28	ralrimiva	$⊢ R Se A \to \forall x \in A Pred (t++ ({R ↾}_{A}), A, x) \in V$
30		dfse3	$⊢ t++ ({R ↾}_{A}) Se A \leftrightarrow \forall x \in A Pred (t++ ({R ↾}_{A}), A, x) \in V$
31	29 30	sylibr	$⊢ R Se A \to t++ ({R ↾}_{A}) Se A$

Metamath Proof Explorer

Theorem ttrclse

Proof