rtrclreclem4

Description: The reflexive, transitive closure of R is the smallest reflexive, transitive relation which contains R and the identity. (Contributed by Drahflow, 12-Nov-2015) (Revised by RP, 30-May-2020) (Revised by AV, 13-Jul-2024)

		Ref	Expression
	Hypothesis	rtrclreclem.1	$⊢ φ \to Rel R$
	Assertion	rtrclreclem4	$⊢ φ \to \forall s (({I ↾}_{(dom R \cup ran R)} \subseteq s \land R \subseteq s \land s \circ s \subseteq s) \to t*rec (R) \subseteq s)$

Proof

Step	Hyp	Ref	Expression
1		rtrclreclem.1	$⊢ φ \to Rel R$
2		eqidd	$⊢ (φ \land R \in V) \to (r \in V ⟼ ⋃_{n \in ℕ_{0}} (r ↑_{r} n)) = (r \in V ⟼ ⋃_{n \in ℕ_{0}} (r ↑_{r} n))$
3		oveq1	$⊢ r = R \to r ↑_{r} n = R ↑_{r} n$
4	3	iuneq2d	$⊢ r = R \to ⋃_{n \in ℕ_{0}} (r ↑_{r} n) = ⋃_{n \in ℕ_{0}} (R ↑_{r} n)$
5	4	adantl	$⊢ ((φ \land R \in V) \land r = R) \to ⋃_{n \in ℕ_{0}} (r ↑_{r} n) = ⋃_{n \in ℕ_{0}} (R ↑_{r} n)$
6		simpr	$⊢ (φ \land R \in V) \to R \in V$
7		nn0ex	$⊢ ℕ_{0} \in V$
8		ovex	$⊢ R ↑_{r} n \in V$
9	7 8	iunex	$⊢ ⋃_{n \in ℕ_{0}} (R ↑_{r} n) \in V$
10	9	a1i	$⊢ (φ \land R \in V) \to ⋃_{n \in ℕ_{0}} (R ↑_{r} n) \in V$
11	2 5 6 10	fvmptd	$⊢ (φ \land R \in V) \to (r \in V ⟼ ⋃_{n \in ℕ_{0}} (r ↑_{r} n)) (R) = ⋃_{n \in ℕ_{0}} (R ↑_{r} n)$
12		eleq1	$⊢ i = 0 \to (i \in ℕ_{0} \leftrightarrow 0 \in ℕ_{0})$
13	12	anbi1d	$⊢ i = 0 \to ((i \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land {I ↾}_{(dom R \cup ran R)} \subseteq s)))) \leftrightarrow (0 \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land {I ↾}_{(dom R \cup ran R)} \subseteq s)))))$
14		oveq2	$⊢ i = 0 \to R ↑_{r} i = R ↑_{r} 0$
15	14	sseq1d	$⊢ i = 0 \to (R ↑_{r} i \subseteq s \leftrightarrow R ↑_{r} 0 \subseteq s)$
16	13 15	imbi12d	$⊢ i = 0 \to (((i \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land {I ↾}_{(dom R \cup ran R)} \subseteq s)))) \to R ↑_{r} i \subseteq s) \leftrightarrow ((0 \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land {I ↾}_{(dom R \cup ran R)} \subseteq s)))) \to R ↑_{r} 0 \subseteq s))$
17		eleq1	$⊢ i = m \to (i \in ℕ_{0} \leftrightarrow m \in ℕ_{0})$
18	17	anbi1d	$⊢ i = m \to ((i \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land {I ↾}_{(dom R \cup ran R)} \subseteq s)))) \leftrightarrow (m \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land {I ↾}_{(dom R \cup ran R)} \subseteq s)))))$
19		oveq2	$⊢ i = m \to R ↑_{r} i = R ↑_{r} m$
20	19	sseq1d	$⊢ i = m \to (R ↑_{r} i \subseteq s \leftrightarrow R ↑_{r} m \subseteq s)$
21	18 20	imbi12d	$⊢ i = m \to (((i \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land {I ↾}_{(dom R \cup ran R)} \subseteq s)))) \to R ↑_{r} i \subseteq s) \leftrightarrow ((m \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land {I ↾}_{(dom R \cup ran R)} \subseteq s)))) \to R ↑_{r} m \subseteq s))$
22		eleq1	$⊢ i = m + 1 \to (i \in ℕ_{0} \leftrightarrow m + 1 \in ℕ_{0})$
23	22	anbi1d	$⊢ i = m + 1 \to ((i \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land {I ↾}_{(dom R \cup ran R)} \subseteq s)))) \leftrightarrow (m + 1 \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land {I ↾}_{(dom R \cup ran R)} \subseteq s)))))$
24		oveq2	$⊢ i = m + 1 \to R ↑_{r} i = R ↑_{r} (m + 1)$
25	24	sseq1d	$⊢ i = m + 1 \to (R ↑_{r} i \subseteq s \leftrightarrow R ↑_{r} (m + 1) \subseteq s)$
26	23 25	imbi12d	$⊢ i = m + 1 \to (((i \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land {I ↾}_{(dom R \cup ran R)} \subseteq s)))) \to R ↑_{r} i \subseteq s) \leftrightarrow ((m + 1 \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land {I ↾}_{(dom R \cup ran R)} \subseteq s)))) \to R ↑_{r} (m + 1) \subseteq s))$
27		eleq1	$⊢ i = n \to (i \in ℕ_{0} \leftrightarrow n \in ℕ_{0})$
28	27	anbi1d	$⊢ i = n \to ((i \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land {I ↾}_{(dom R \cup ran R)} \subseteq s)))) \leftrightarrow (n \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land {I ↾}_{(dom R \cup ran R)} \subseteq s)))))$
29		oveq2	$⊢ i = n \to R ↑_{r} i = R ↑_{r} n$
30	29	sseq1d	$⊢ i = n \to (R ↑_{r} i \subseteq s \leftrightarrow R ↑_{r} n \subseteq s)$
31	28 30	imbi12d	$⊢ i = n \to (((i \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land {I ↾}_{(dom R \cup ran R)} \subseteq s)))) \to R ↑_{r} i \subseteq s) \leftrightarrow ((n \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land {I ↾}_{(dom R \cup ran R)} \subseteq s)))) \to R ↑_{r} n \subseteq s))$
32		simprll	$⊢ (0 \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land {I ↾}_{(dom R \cup ran R)} \subseteq s)))) \to φ$
33	32 1	syl	$⊢ (0 \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land {I ↾}_{(dom R \cup ran R)} \subseteq s)))) \to Rel R$
34		simprlr	$⊢ (0 \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land {I ↾}_{(dom R \cup ran R)} \subseteq s)))) \to R \in V$
35	33 34	relexp0d	$⊢ (0 \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land {I ↾}_{(dom R \cup ran R)} \subseteq s)))) \to R ↑_{r} 0 = {I ↾}_{⋃ ⋃ R}$
36		relfld	$⊢ Rel R \to ⋃ ⋃ R = dom R \cup ran R$
37	33 36	syl	$⊢ (0 \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land {I ↾}_{(dom R \cup ran R)} \subseteq s)))) \to ⋃ ⋃ R = dom R \cup ran R$
38		simprrr	$⊢ ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land {I ↾}_{(dom R \cup ran R)} \subseteq s))) \to {I ↾}_{(dom R \cup ran R)} \subseteq s$
39	38	adantl	$⊢ (0 \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land {I ↾}_{(dom R \cup ran R)} \subseteq s)))) \to {I ↾}_{(dom R \cup ran R)} \subseteq s$
40		reseq2	$⊢ ⋃ ⋃ R = dom R \cup ran R \to {I ↾}_{⋃ ⋃ R} = {I ↾}_{(dom R \cup ran R)}$
41	40	sseq1d	$⊢ ⋃ ⋃ R = dom R \cup ran R \to ({I ↾}_{⋃ ⋃ R} \subseteq s \leftrightarrow {I ↾}_{(dom R \cup ran R)} \subseteq s)$
42	39 41	imbitrrid	$⊢ ⋃ ⋃ R = dom R \cup ran R \to ((0 \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land {I ↾}_{(dom R \cup ran R)} \subseteq s)))) \to {I ↾}_{⋃ ⋃ R} \subseteq s)$
43	37 42	mpcom	$⊢ (0 \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land {I ↾}_{(dom R \cup ran R)} \subseteq s)))) \to {I ↾}_{⋃ ⋃ R} \subseteq s$
44	35 43	eqsstrd	$⊢ (0 \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land {I ↾}_{(dom R \cup ran R)} \subseteq s)))) \to R ↑_{r} 0 \subseteq s$
45		simprrr	$⊢ (R \subseteq s \land ({I ↾}_{(dom R \cup ran R)} \subseteq s \land (((m \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land {I ↾}_{(dom R \cup ran R)} \subseteq s)))) \to R ↑_{r} m \subseteq s) \land m \in ℕ_{0}))) \to m \in ℕ_{0}$
46	45	adantl	$⊢ (s \circ s \subseteq s \land (R \subseteq s \land ({I ↾}_{(dom R \cup ran R)} \subseteq s \land (((m \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land {I ↾}_{(dom R \cup ran R)} \subseteq s)))) \to R ↑_{r} m \subseteq s) \land m \in ℕ_{0})))) \to m \in ℕ_{0}$
47	46	adantl	$⊢ ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land ({I ↾}_{(dom R \cup ran R)} \subseteq s \land (((m \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land {I ↾}_{(dom R \cup ran R)} \subseteq s)))) \to R ↑_{r} m \subseteq s) \land m \in ℕ_{0}))))) \to m \in ℕ_{0}$
48	47	adantl	$⊢ (m + 1 \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land ({I ↾}_{(dom R \cup ran R)} \subseteq s \land (((m \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land {I ↾}_{(dom R \cup ran R)} \subseteq s)))) \to R ↑_{r} m \subseteq s) \land m \in ℕ_{0})))))) \to m \in ℕ_{0}$
49		simprl	$⊢ (m + 1 \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land ({I ↾}_{(dom R \cup ran R)} \subseteq s \land (((m \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land {I ↾}_{(dom R \cup ran R)} \subseteq s)))) \to R ↑_{r} m \subseteq s) \land m \in ℕ_{0})))))) \to (φ \land R \in V)$
50		simprrl	$⊢ (m + 1 \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land ({I ↾}_{(dom R \cup ran R)} \subseteq s \land (((m \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land {I ↾}_{(dom R \cup ran R)} \subseteq s)))) \to R ↑_{r} m \subseteq s) \land m \in ℕ_{0})))))) \to s \circ s \subseteq s$
51		simprrl	$⊢ ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land ({I ↾}_{(dom R \cup ran R)} \subseteq s \land (((m \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land {I ↾}_{(dom R \cup ran R)} \subseteq s)))) \to R ↑_{r} m \subseteq s) \land m \in ℕ_{0}))))) \to R \subseteq s$
52	51	adantl	$⊢ (m + 1 \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land ({I ↾}_{(dom R \cup ran R)} \subseteq s \land (((m \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land {I ↾}_{(dom R \cup ran R)} \subseteq s)))) \to R ↑_{r} m \subseteq s) \land m \in ℕ_{0})))))) \to R \subseteq s$
53		simprrl	$⊢ (s \circ s \subseteq s \land (R \subseteq s \land ({I ↾}_{(dom R \cup ran R)} \subseteq s \land (((m \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land {I ↾}_{(dom R \cup ran R)} \subseteq s)))) \to R ↑_{r} m \subseteq s) \land m \in ℕ_{0})))) \to {I ↾}_{(dom R \cup ran R)} \subseteq s$
54	53	adantl	$⊢ ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land ({I ↾}_{(dom R \cup ran R)} \subseteq s \land (((m \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land {I ↾}_{(dom R \cup ran R)} \subseteq s)))) \to R ↑_{r} m \subseteq s) \land m \in ℕ_{0}))))) \to {I ↾}_{(dom R \cup ran R)} \subseteq s$
55	54	adantl	$⊢ (m + 1 \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land ({I ↾}_{(dom R \cup ran R)} \subseteq s \land (((m \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land {I ↾}_{(dom R \cup ran R)} \subseteq s)))) \to R ↑_{r} m \subseteq s) \land m \in ℕ_{0})))))) \to {I ↾}_{(dom R \cup ran R)} \subseteq s$
56	50 52 55	jca32	$⊢ (m + 1 \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land ({I ↾}_{(dom R \cup ran R)} \subseteq s \land (((m \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land {I ↾}_{(dom R \cup ran R)} \subseteq s)))) \to R ↑_{r} m \subseteq s) \land m \in ℕ_{0})))))) \to (s \circ s \subseteq s \land (R \subseteq s \land {I ↾}_{(dom R \cup ran R)} \subseteq s))$
57	48 49 56	jca32	$⊢ (m + 1 \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land ({I ↾}_{(dom R \cup ran R)} \subseteq s \land (((m \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land {I ↾}_{(dom R \cup ran R)} \subseteq s)))) \to R ↑_{r} m \subseteq s) \land m \in ℕ_{0})))))) \to (m \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land {I ↾}_{(dom R \cup ran R)} \subseteq s))))$
58		simprrl	$⊢ (R \subseteq s \land ({I ↾}_{(dom R \cup ran R)} \subseteq s \land (((m \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land {I ↾}_{(dom R \cup ran R)} \subseteq s)))) \to R ↑_{r} m \subseteq s) \land m \in ℕ_{0}))) \to ((m \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land {I ↾}_{(dom R \cup ran R)} \subseteq s)))) \to R ↑_{r} m \subseteq s)$
59	58	adantl	$⊢ (s \circ s \subseteq s \land (R \subseteq s \land ({I ↾}_{(dom R \cup ran R)} \subseteq s \land (((m \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land {I ↾}_{(dom R \cup ran R)} \subseteq s)))) \to R ↑_{r} m \subseteq s) \land m \in ℕ_{0})))) \to ((m \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land {I ↾}_{(dom R \cup ran R)} \subseteq s)))) \to R ↑_{r} m \subseteq s)$
60	59	adantl	$⊢ ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land ({I ↾}_{(dom R \cup ran R)} \subseteq s \land (((m \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land {I ↾}_{(dom R \cup ran R)} \subseteq s)))) \to R ↑_{r} m \subseteq s) \land m \in ℕ_{0}))))) \to ((m \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land {I ↾}_{(dom R \cup ran R)} \subseteq s)))) \to R ↑_{r} m \subseteq s)$
61	60	adantl	$⊢ (m + 1 \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land ({I ↾}_{(dom R \cup ran R)} \subseteq s \land (((m \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land {I ↾}_{(dom R \cup ran R)} \subseteq s)))) \to R ↑_{r} m \subseteq s) \land m \in ℕ_{0})))))) \to ((m \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land {I ↾}_{(dom R \cup ran R)} \subseteq s)))) \to R ↑_{r} m \subseteq s)$
62	57 61	mpd	$⊢ (m + 1 \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land ({I ↾}_{(dom R \cup ran R)} \subseteq s \land (((m \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land {I ↾}_{(dom R \cup ran R)} \subseteq s)))) \to R ↑_{r} m \subseteq s) \land m \in ℕ_{0})))))) \to R ↑_{r} m \subseteq s$
63		simprll	$⊢ (m + 1 \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land ({I ↾}_{(dom R \cup ran R)} \subseteq s \land (((m \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land {I ↾}_{(dom R \cup ran R)} \subseteq s)))) \to R ↑_{r} m \subseteq s) \land m \in ℕ_{0})))))) \to φ$
64	63	adantl	$⊢ (R ↑_{r} m \subseteq s \land (m + 1 \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land ({I ↾}_{(dom R \cup ran R)} \subseteq s \land (((m \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land {I ↾}_{(dom R \cup ran R)} \subseteq s)))) \to R ↑_{r} m \subseteq s) \land m \in ℕ_{0}))))))) \to φ$
65	64 1	syl	$⊢ (R ↑_{r} m \subseteq s \land (m + 1 \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land ({I ↾}_{(dom R \cup ran R)} \subseteq s \land (((m \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land {I ↾}_{(dom R \cup ran R)} \subseteq s)))) \to R ↑_{r} m \subseteq s) \land m \in ℕ_{0}))))))) \to Rel R$
66	48	adantl	$⊢ (R ↑_{r} m \subseteq s \land (m + 1 \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land ({I ↾}_{(dom R \cup ran R)} \subseteq s \land (((m \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land {I ↾}_{(dom R \cup ran R)} \subseteq s)))) \to R ↑_{r} m \subseteq s) \land m \in ℕ_{0}))))))) \to m \in ℕ_{0}$
67	65 66	relexpsucrd	$⊢ (R ↑_{r} m \subseteq s \land (m + 1 \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land ({I ↾}_{(dom R \cup ran R)} \subseteq s \land (((m \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land {I ↾}_{(dom R \cup ran R)} \subseteq s)))) \to R ↑_{r} m \subseteq s) \land m \in ℕ_{0}))))))) \to R ↑_{r} (m + 1) = (R ↑_{r} m) \circ R$
68	52	adantl	$⊢ (R ↑_{r} m \subseteq s \land (m + 1 \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land ({I ↾}_{(dom R \cup ran R)} \subseteq s \land (((m \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land {I ↾}_{(dom R \cup ran R)} \subseteq s)))) \to R ↑_{r} m \subseteq s) \land m \in ℕ_{0}))))))) \to R \subseteq s$
69		coss2	$⊢ R \subseteq s \to (R ↑_{r} m) \circ R \subseteq (R ↑_{r} m) \circ s$
70	68 69	syl	$⊢ (R ↑_{r} m \subseteq s \land (m + 1 \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land ({I ↾}_{(dom R \cup ran R)} \subseteq s \land (((m \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land {I ↾}_{(dom R \cup ran R)} \subseteq s)))) \to R ↑_{r} m \subseteq s) \land m \in ℕ_{0}))))))) \to (R ↑_{r} m) \circ R \subseteq (R ↑_{r} m) \circ s$
71		coss1	$⊢ R ↑_{r} m \subseteq s \to (R ↑_{r} m) \circ s \subseteq s \circ s$
72	71 50	sylan9ss	$⊢ (R ↑_{r} m \subseteq s \land (m + 1 \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land ({I ↾}_{(dom R \cup ran R)} \subseteq s \land (((m \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land {I ↾}_{(dom R \cup ran R)} \subseteq s)))) \to R ↑_{r} m \subseteq s) \land m \in ℕ_{0}))))))) \to (R ↑_{r} m) \circ s \subseteq s$
73	70 72	sstrd	$⊢ (R ↑_{r} m \subseteq s \land (m + 1 \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land ({I ↾}_{(dom R \cup ran R)} \subseteq s \land (((m \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land {I ↾}_{(dom R \cup ran R)} \subseteq s)))) \to R ↑_{r} m \subseteq s) \land m \in ℕ_{0}))))))) \to (R ↑_{r} m) \circ R \subseteq s$
74	67 73	eqsstrd	$⊢ (R ↑_{r} m \subseteq s \land (m + 1 \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land ({I ↾}_{(dom R \cup ran R)} \subseteq s \land (((m \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land {I ↾}_{(dom R \cup ran R)} \subseteq s)))) \to R ↑_{r} m \subseteq s) \land m \in ℕ_{0}))))))) \to R ↑_{r} (m + 1) \subseteq s$
75	62 74	mpancom	$⊢ (m + 1 \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land ({I ↾}_{(dom R \cup ran R)} \subseteq s \land (((m \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land {I ↾}_{(dom R \cup ran R)} \subseteq s)))) \to R ↑_{r} m \subseteq s) \land m \in ℕ_{0})))))) \to R ↑_{r} (m + 1) \subseteq s$
76	75	expcom	$⊢ ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land ({I ↾}_{(dom R \cup ran R)} \subseteq s \land (((m \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land {I ↾}_{(dom R \cup ran R)} \subseteq s)))) \to R ↑_{r} m \subseteq s) \land m \in ℕ_{0}))))) \to (m + 1 \in ℕ_{0} \to R ↑_{r} (m + 1) \subseteq s)$
77	76	expcom	$⊢ (s \circ s \subseteq s \land (R \subseteq s \land ({I ↾}_{(dom R \cup ran R)} \subseteq s \land (((m \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land {I ↾}_{(dom R \cup ran R)} \subseteq s)))) \to R ↑_{r} m \subseteq s) \land m \in ℕ_{0})))) \to ((φ \land R \in V) \to (m + 1 \in ℕ_{0} \to R ↑_{r} (m + 1) \subseteq s))$
78	77	expcom	$⊢ (R \subseteq s \land ({I ↾}_{(dom R \cup ran R)} \subseteq s \land (((m \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land {I ↾}_{(dom R \cup ran R)} \subseteq s)))) \to R ↑_{r} m \subseteq s) \land m \in ℕ_{0}))) \to (s \circ s \subseteq s \to ((φ \land R \in V) \to (m + 1 \in ℕ_{0} \to R ↑_{r} (m + 1) \subseteq s)))$
79	78	anassrs	$⊢ ((R \subseteq s \land {I ↾}_{(dom R \cup ran R)} \subseteq s) \land (((m \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land {I ↾}_{(dom R \cup ran R)} \subseteq s)))) \to R ↑_{r} m \subseteq s) \land m \in ℕ_{0})) \to (s \circ s \subseteq s \to ((φ \land R \in V) \to (m + 1 \in ℕ_{0} \to R ↑_{r} (m + 1) \subseteq s)))$
80	79	impcom	$⊢ (s \circ s \subseteq s \land ((R \subseteq s \land {I ↾}_{(dom R \cup ran R)} \subseteq s) \land (((m \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land {I ↾}_{(dom R \cup ran R)} \subseteq s)))) \to R ↑_{r} m \subseteq s) \land m \in ℕ_{0}))) \to ((φ \land R \in V) \to (m + 1 \in ℕ_{0} \to R ↑_{r} (m + 1) \subseteq s))$
81	80	anassrs	$⊢ ((s \circ s \subseteq s \land (R \subseteq s \land {I ↾}_{(dom R \cup ran R)} \subseteq s)) \land (((m \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land {I ↾}_{(dom R \cup ran R)} \subseteq s)))) \to R ↑_{r} m \subseteq s) \land m \in ℕ_{0})) \to ((φ \land R \in V) \to (m + 1 \in ℕ_{0} \to R ↑_{r} (m + 1) \subseteq s))$
82	81	impcom	$⊢ ((φ \land R \in V) \land ((s \circ s \subseteq s \land (R \subseteq s \land {I ↾}_{(dom R \cup ran R)} \subseteq s)) \land (((m \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land {I ↾}_{(dom R \cup ran R)} \subseteq s)))) \to R ↑_{r} m \subseteq s) \land m \in ℕ_{0}))) \to (m + 1 \in ℕ_{0} \to R ↑_{r} (m + 1) \subseteq s)$
83	82	anassrs	$⊢ (((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land {I ↾}_{(dom R \cup ran R)} \subseteq s))) \land (((m \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land {I ↾}_{(dom R \cup ran R)} \subseteq s)))) \to R ↑_{r} m \subseteq s) \land m \in ℕ_{0})) \to (m + 1 \in ℕ_{0} \to R ↑_{r} (m + 1) \subseteq s)$
84	83	impcom	$⊢ (m + 1 \in ℕ_{0} \land (((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land {I ↾}_{(dom R \cup ran R)} \subseteq s))) \land (((m \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land {I ↾}_{(dom R \cup ran R)} \subseteq s)))) \to R ↑_{r} m \subseteq s) \land m \in ℕ_{0}))) \to R ↑_{r} (m + 1) \subseteq s$
85	84	anassrs	$⊢ ((m + 1 \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land {I ↾}_{(dom R \cup ran R)} \subseteq s)))) \land (((m \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land {I ↾}_{(dom R \cup ran R)} \subseteq s)))) \to R ↑_{r} m \subseteq s) \land m \in ℕ_{0})) \to R ↑_{r} (m + 1) \subseteq s$
86	85	expcom	$⊢ (((m \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land {I ↾}_{(dom R \cup ran R)} \subseteq s)))) \to R ↑_{r} m \subseteq s) \land m \in ℕ_{0}) \to ((m + 1 \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land {I ↾}_{(dom R \cup ran R)} \subseteq s)))) \to R ↑_{r} (m + 1) \subseteq s)$
87	86	expcom	$⊢ m \in ℕ_{0} \to (((m \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land {I ↾}_{(dom R \cup ran R)} \subseteq s)))) \to R ↑_{r} m \subseteq s) \to ((m + 1 \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land {I ↾}_{(dom R \cup ran R)} \subseteq s)))) \to R ↑_{r} (m + 1) \subseteq s))$
88	16 21 26 31 44 87	nn0ind	$⊢ n \in ℕ_{0} \to ((n \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land {I ↾}_{(dom R \cup ran R)} \subseteq s)))) \to R ↑_{r} n \subseteq s)$
89	88	anabsi5	$⊢ (n \in ℕ_{0} \land ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land {I ↾}_{(dom R \cup ran R)} \subseteq s)))) \to R ↑_{r} n \subseteq s$
90	89	expcom	$⊢ ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land {I ↾}_{(dom R \cup ran R)} \subseteq s))) \to (n \in ℕ_{0} \to R ↑_{r} n \subseteq s)$
91	90	ralrimiv	$⊢ ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land {I ↾}_{(dom R \cup ran R)} \subseteq s))) \to \forall n \in ℕ_{0} R ↑_{r} n \subseteq s$
92		iunss	$⊢ ⋃_{n \in ℕ_{0}} (R ↑_{r} n) \subseteq s \leftrightarrow \forall n \in ℕ_{0} R ↑_{r} n \subseteq s$
93	91 92	sylibr	$⊢ ((φ \land R \in V) \land (s \circ s \subseteq s \land (R \subseteq s \land {I ↾}_{(dom R \cup ran R)} \subseteq s))) \to ⋃_{n \in ℕ_{0}} (R ↑_{r} n) \subseteq s$
94	93	expcom	$⊢ (s \circ s \subseteq s \land (R \subseteq s \land {I ↾}_{(dom R \cup ran R)} \subseteq s)) \to ((φ \land R \in V) \to ⋃_{n \in ℕ_{0}} (R ↑_{r} n) \subseteq s)$
95	94	expcom	$⊢ (R \subseteq s \land {I ↾}_{(dom R \cup ran R)} \subseteq s) \to (s \circ s \subseteq s \to ((φ \land R \in V) \to ⋃_{n \in ℕ_{0}} (R ↑_{r} n) \subseteq s))$
96	95	expcom	$⊢ {I ↾}_{(dom R \cup ran R)} \subseteq s \to (R \subseteq s \to (s \circ s \subseteq s \to ((φ \land R \in V) \to ⋃_{n \in ℕ_{0}} (R ↑_{r} n) \subseteq s)))$
97	96	3imp1	$⊢ (({I ↾}_{(dom R \cup ran R)} \subseteq s \land R \subseteq s \land s \circ s \subseteq s) \land (φ \land R \in V)) \to ⋃_{n \in ℕ_{0}} (R ↑_{r} n) \subseteq s$
98	97	expcom	$⊢ (φ \land R \in V) \to (({I ↾}_{(dom R \cup ran R)} \subseteq s \land R \subseteq s \land s \circ s \subseteq s) \to ⋃_{n \in ℕ_{0}} (R ↑_{r} n) \subseteq s)$
99		sseq1	$⊢ (r \in V ⟼ ⋃_{n \in ℕ_{0}} (r ↑_{r} n)) (R) = ⋃_{n \in ℕ_{0}} (R ↑_{r} n) \to ((r \in V ⟼ ⋃_{n \in ℕ_{0}} (r ↑_{r} n)) (R) \subseteq s \leftrightarrow ⋃_{n \in ℕ_{0}} (R ↑_{r} n) \subseteq s)$
100	99	imbi2d	$⊢ (r \in V ⟼ ⋃_{n \in ℕ_{0}} (r ↑_{r} n)) (R) = ⋃_{n \in ℕ_{0}} (R ↑_{r} n) \to ((({I ↾}_{(dom R \cup ran R)} \subseteq s \land R \subseteq s \land s \circ s \subseteq s) \to (r \in V ⟼ ⋃_{n \in ℕ_{0}} (r ↑_{r} n)) (R) \subseteq s) \leftrightarrow (({I ↾}_{(dom R \cup ran R)} \subseteq s \land R \subseteq s \land s \circ s \subseteq s) \to ⋃_{n \in ℕ_{0}} (R ↑_{r} n) \subseteq s))$
101	98 100	imbitrrid	$⊢ (r \in V ⟼ ⋃_{n \in ℕ_{0}} (r ↑_{r} n)) (R) = ⋃_{n \in ℕ_{0}} (R ↑_{r} n) \to ((φ \land R \in V) \to (({I ↾}_{(dom R \cup ran R)} \subseteq s \land R \subseteq s \land s \circ s \subseteq s) \to (r \in V ⟼ ⋃_{n \in ℕ_{0}} (r ↑_{r} n)) (R) \subseteq s))$
102	11 101	mpcom	$⊢ (φ \land R \in V) \to (({I ↾}_{(dom R \cup ran R)} \subseteq s \land R \subseteq s \land s \circ s \subseteq s) \to (r \in V ⟼ ⋃_{n \in ℕ_{0}} (r ↑_{r} n)) (R) \subseteq s)$
103		df-rtrclrec	$⊢ t*rec = (r \in V ⟼ ⋃_{n \in ℕ_{0}} (r ↑_{r} n))$
104		fveq1	$⊢ trec = (r \in V ⟼ ⋃_{n \in ℕ_{0}} (r ↑_{r} n)) \to trec (R) = (r \in V ⟼ ⋃_{n \in ℕ_{0}} (r ↑_{r} n)) (R)$
105	104	sseq1d	$⊢ trec = (r \in V ⟼ ⋃_{n \in ℕ_{0}} (r ↑_{r} n)) \to (trec (R) \subseteq s \leftrightarrow (r \in V ⟼ ⋃_{n \in ℕ_{0}} (r ↑_{r} n)) (R) \subseteq s)$
106	105	imbi2d	$⊢ trec = (r \in V ⟼ ⋃_{n \in ℕ_{0}} (r ↑_{r} n)) \to ((({I ↾}_{(dom R \cup ran R)} \subseteq s \land R \subseteq s \land s \circ s \subseteq s) \to trec (R) \subseteq s) \leftrightarrow (({I ↾}_{(dom R \cup ran R)} \subseteq s \land R \subseteq s \land s \circ s \subseteq s) \to (r \in V ⟼ ⋃_{n \in ℕ_{0}} (r ↑_{r} n)) (R) \subseteq s))$
107	106	imbi2d	$⊢ trec = (r \in V ⟼ ⋃_{n \in ℕ_{0}} (r ↑_{r} n)) \to (((φ \land R \in V) \to (({I ↾}_{(dom R \cup ran R)} \subseteq s \land R \subseteq s \land s \circ s \subseteq s) \to trec (R) \subseteq s)) \leftrightarrow ((φ \land R \in V) \to (({I ↾}_{(dom R \cup ran R)} \subseteq s \land R \subseteq s \land s \circ s \subseteq s) \to (r \in V ⟼ ⋃_{n \in ℕ_{0}} (r ↑_{r} n)) (R) \subseteq s)))$
108	103 107	ax-mp	$⊢ ((φ \land R \in V) \to (({I ↾}_{(dom R \cup ran R)} \subseteq s \land R \subseteq s \land s \circ s \subseteq s) \to t*rec (R) \subseteq s)) \leftrightarrow ((φ \land R \in V) \to (({I ↾}_{(dom R \cup ran R)} \subseteq s \land R \subseteq s \land s \circ s \subseteq s) \to (r \in V ⟼ ⋃_{n \in ℕ_{0}} (r ↑_{r} n)) (R) \subseteq s))$
109	102 108	mpbir	$⊢ (φ \land R \in V) \to (({I ↾}_{(dom R \cup ran R)} \subseteq s \land R \subseteq s \land s \circ s \subseteq s) \to t*rec (R) \subseteq s)$
110	109	ex	$⊢ φ \to (R \in V \to (({I ↾}_{(dom R \cup ran R)} \subseteq s \land R \subseteq s \land s \circ s \subseteq s) \to t*rec (R) \subseteq s))$
111		fvprc	$⊢ \neg R \in V \to t*rec (R) = \emptyset$
112		0ss	$⊢ \emptyset \subseteq s$
113	111 112	eqsstrdi	$⊢ \neg R \in V \to t*rec (R) \subseteq s$
114	113	a1d	$⊢ \neg R \in V \to (({I ↾}_{(dom R \cup ran R)} \subseteq s \land R \subseteq s \land s \circ s \subseteq s) \to t*rec (R) \subseteq s)$
115	110 114	pm2.61d1	$⊢ φ \to (({I ↾}_{(dom R \cup ran R)} \subseteq s \land R \subseteq s \land s \circ s \subseteq s) \to t*rec (R) \subseteq s)$
116	115	alrimiv	$⊢ φ \to \forall s (({I ↾}_{(dom R \cup ran R)} \subseteq s \land R \subseteq s \land s \circ s \subseteq s) \to t*rec (R) \subseteq s)$

Metamath Proof Explorer

Theorem rtrclreclem4

Proof