rtrclreclem3

Description: The reflexive, transitive closure is indeed transitive. (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	rtrclreclem3	$⊢ φ \to trec (R) \circ trec (R) \subseteq t*rec (R)$

Proof

Step	Hyp	Ref	Expression
1		rtrclreclem.1	$⊢ φ \to Rel R$
2		df-co	$⊢ trec (R) \circ trec (R) = \{⟨e, g⟩ \| \exists f (e trec (R) f \land f trec (R) g)\}$
3		elopab	$⊢ d \in \{⟨e, g⟩ \| \exists f (e trec (R) f \land f trec (R) g)\} \leftrightarrow \exists e \exists g (d = ⟨e, g⟩ \land \exists f (e trec (R) f \land f trec (R) g))$
4		eqeq1	$⊢ d = ⟨e, g⟩ \to (d = ⟨e, g⟩ \leftrightarrow ⟨e, g⟩ = ⟨e, g⟩)$
5	4	anbi1d	$⊢ d = ⟨e, g⟩ \to ((d = ⟨e, g⟩ \land (\exists f (e trec (R) f \land f trec (R) g) \land φ)) \leftrightarrow (⟨e, g⟩ = ⟨e, g⟩ \land (\exists f (e trec (R) f \land f trec (R) g) \land φ)))$
6		simprr	$⊢ (⟨e, g⟩ = ⟨e, g⟩ \land (\exists f (e trec (R) f \land f trec (R) g) \land φ)) \to φ$
7		simprl	$⊢ (⟨e, g⟩ = ⟨e, g⟩ \land (\exists f (e trec (R) f \land f trec (R) g) \land φ)) \to \exists f (e trec (R) f \land f trec (R) g)$
8		simpl	$⊢ (e trec (R) f \land (f trec (R) g \land φ)) \to e t*rec (R) f$
9		simprr	$⊢ (e trec (R) f \land (f trec (R) g \land φ)) \to φ$
10	1	dfrtrclrec2	$⊢ φ \to (e t*rec (R) f \leftrightarrow \exists n \in ℕ_{0} e (R ↑_{r} n) f)$
11	9 10	syl	$⊢ (e trec (R) f \land (f trec (R) g \land φ)) \to (e t*rec (R) f \leftrightarrow \exists n \in ℕ_{0} e (R ↑_{r} n) f)$
12	8 11	mpbid	$⊢ (e trec (R) f \land (f trec (R) g \land φ)) \to \exists n \in ℕ_{0} e (R ↑_{r} n) f$
13		simprl	$⊢ (e trec (R) f \land (f trec (R) g \land (φ \land (e (R ↑_{r} n) f \land n \in ℕ_{0})))) \to f t*rec (R) g$
14		simprrl	$⊢ (e trec (R) f \land (f trec (R) g \land (φ \land (e (R ↑_{r} n) f \land n \in ℕ_{0})))) \to φ$
15	1	dfrtrclrec2	$⊢ φ \to (f t*rec (R) g \leftrightarrow \exists m \in ℕ_{0} f (R ↑_{r} m) g)$
16	14 15	syl	$⊢ (e trec (R) f \land (f trec (R) g \land (φ \land (e (R ↑_{r} n) f \land n \in ℕ_{0})))) \to (f t*rec (R) g \leftrightarrow \exists m \in ℕ_{0} f (R ↑_{r} m) g)$
17	13 16	mpbid	$⊢ (e trec (R) f \land (f trec (R) g \land (φ \land (e (R ↑_{r} n) f \land n \in ℕ_{0})))) \to \exists m \in ℕ_{0} f (R ↑_{r} m) g$
18		simprrl	$⊢ (φ \land (e (R ↑_{r} n) f \land (n \in ℕ_{0} \land (f (R ↑_{r} m) g \land m \in ℕ_{0})))) \to n \in ℕ_{0}$
19	18	adantl	$⊢ (f t*rec (R) g \land (φ \land (e (R ↑_{r} n) f \land (n \in ℕ_{0} \land (f (R ↑_{r} m) g \land m \in ℕ_{0}))))) \to n \in ℕ_{0}$
20	19	adantl	$⊢ (e trec (R) f \land (f trec (R) g \land (φ \land (e (R ↑_{r} n) f \land (n \in ℕ_{0} \land (f (R ↑_{r} m) g \land m \in ℕ_{0})))))) \to n \in ℕ_{0}$
21		simprr	$⊢ (n \in ℕ_{0} \land (f (R ↑_{r} m) g \land m \in ℕ_{0})) \to m \in ℕ_{0}$
22	21	adantl	$⊢ (e (R ↑_{r} n) f \land (n \in ℕ_{0} \land (f (R ↑_{r} m) g \land m \in ℕ_{0}))) \to m \in ℕ_{0}$
23	22	adantl	$⊢ (φ \land (e (R ↑_{r} n) f \land (n \in ℕ_{0} \land (f (R ↑_{r} m) g \land m \in ℕ_{0})))) \to m \in ℕ_{0}$
24	23	adantl	$⊢ (f t*rec (R) g \land (φ \land (e (R ↑_{r} n) f \land (n \in ℕ_{0} \land (f (R ↑_{r} m) g \land m \in ℕ_{0}))))) \to m \in ℕ_{0}$
25	24	adantl	$⊢ (e trec (R) f \land (f trec (R) g \land (φ \land (e (R ↑_{r} n) f \land (n \in ℕ_{0} \land (f (R ↑_{r} m) g \land m \in ℕ_{0})))))) \to m \in ℕ_{0}$
26	20 25	nn0addcld	$⊢ (e trec (R) f \land (f trec (R) g \land (φ \land (e (R ↑_{r} n) f \land (n \in ℕ_{0} \land (f (R ↑_{r} m) g \land m \in ℕ_{0})))))) \to n + m \in ℕ_{0}$
27	20	adantl	$⊢ (n + m \in ℕ_{0} \land (e trec (R) f \land (f trec (R) g \land (φ \land (e (R ↑_{r} n) f \land (n \in ℕ_{0} \land (f (R ↑_{r} m) g \land m \in ℕ_{0}))))))) \to n \in ℕ_{0}$
28	27	nn0cnd	$⊢ (n + m \in ℕ_{0} \land (e trec (R) f \land (f trec (R) g \land (φ \land (e (R ↑_{r} n) f \land (n \in ℕ_{0} \land (f (R ↑_{r} m) g \land m \in ℕ_{0}))))))) \to n \in ℂ$
29	25	adantl	$⊢ (n + m \in ℕ_{0} \land (e trec (R) f \land (f trec (R) g \land (φ \land (e (R ↑_{r} n) f \land (n \in ℕ_{0} \land (f (R ↑_{r} m) g \land m \in ℕ_{0}))))))) \to m \in ℕ_{0}$
30	29	nn0cnd	$⊢ (n + m \in ℕ_{0} \land (e trec (R) f \land (f trec (R) g \land (φ \land (e (R ↑_{r} n) f \land (n \in ℕ_{0} \land (f (R ↑_{r} m) g \land m \in ℕ_{0}))))))) \to m \in ℂ$
31	28 30	addcomd	$⊢ (n + m \in ℕ_{0} \land (e trec (R) f \land (f trec (R) g \land (φ \land (e (R ↑_{r} n) f \land (n \in ℕ_{0} \land (f (R ↑_{r} m) g \land m \in ℕ_{0}))))))) \to n + m = m + n$
32		eleq1	$⊢ n + m = m + n \to (n + m \in ℕ_{0} \leftrightarrow m + n \in ℕ_{0})$
33	32	anbi1d	$⊢ n + m = m + n \to ((n + m \in ℕ_{0} \land (e trec (R) f \land (f trec (R) g \land (φ \land (e (R ↑_{r} n) f \land (n \in ℕ_{0} \land (f (R ↑_{r} m) g \land m \in ℕ_{0}))))))) \leftrightarrow (m + n \in ℕ_{0} \land (e trec (R) f \land (f trec (R) g \land (φ \land (e (R ↑_{r} n) f \land (n \in ℕ_{0} \land (f (R ↑_{r} m) g \land m \in ℕ_{0}))))))))$
34		simprrl	$⊢ (e trec (R) f \land (f trec (R) g \land (φ \land (e (R ↑_{r} n) f \land (n \in ℕ_{0} \land (f (R ↑_{r} m) g \land m \in ℕ_{0})))))) \to φ$
35	34	adantl	$⊢ (m + n \in ℕ_{0} \land (e trec (R) f \land (f trec (R) g \land (φ \land (e (R ↑_{r} n) f \land (n \in ℕ_{0} \land (f (R ↑_{r} m) g \land m \in ℕ_{0}))))))) \to φ$
36	35 1	syl	$⊢ (m + n \in ℕ_{0} \land (e trec (R) f \land (f trec (R) g \land (φ \land (e (R ↑_{r} n) f \land (n \in ℕ_{0} \land (f (R ↑_{r} m) g \land m \in ℕ_{0}))))))) \to Rel R$
37	25	adantl	$⊢ (m + n \in ℕ_{0} \land (e trec (R) f \land (f trec (R) g \land (φ \land (e (R ↑_{r} n) f \land (n \in ℕ_{0} \land (f (R ↑_{r} m) g \land m \in ℕ_{0}))))))) \to m \in ℕ_{0}$
38	20	adantl	$⊢ (m + n \in ℕ_{0} \land (e trec (R) f \land (f trec (R) g \land (φ \land (e (R ↑_{r} n) f \land (n \in ℕ_{0} \land (f (R ↑_{r} m) g \land m \in ℕ_{0}))))))) \to n \in ℕ_{0}$
39	36 37 38	relexpaddd	$⊢ (m + n \in ℕ_{0} \land (e trec (R) f \land (f trec (R) g \land (φ \land (e (R ↑_{r} n) f \land (n \in ℕ_{0} \land (f (R ↑_{r} m) g \land m \in ℕ_{0}))))))) \to (R ↑_{r} m) \circ (R ↑_{r} n) = R ↑_{r} (m + n)$
40		oveq2	$⊢ n + m = m + n \to R ↑_{r} (n + m) = R ↑_{r} (m + n)$
41	40	eqeq2d	$⊢ n + m = m + n \to ((R ↑_{r} m) \circ (R ↑_{r} n) = R ↑_{r} (n + m) \leftrightarrow (R ↑_{r} m) \circ (R ↑_{r} n) = R ↑_{r} (m + n))$
42	39 41	imbitrrid	$⊢ n + m = m + n \to ((m + n \in ℕ_{0} \land (e trec (R) f \land (f trec (R) g \land (φ \land (e (R ↑_{r} n) f \land (n \in ℕ_{0} \land (f (R ↑_{r} m) g \land m \in ℕ_{0}))))))) \to (R ↑_{r} m) \circ (R ↑_{r} n) = R ↑_{r} (n + m))$
43	33 42	sylbid	$⊢ n + m = m + n \to ((n + m \in ℕ_{0} \land (e trec (R) f \land (f trec (R) g \land (φ \land (e (R ↑_{r} n) f \land (n \in ℕ_{0} \land (f (R ↑_{r} m) g \land m \in ℕ_{0}))))))) \to (R ↑_{r} m) \circ (R ↑_{r} n) = R ↑_{r} (n + m))$
44	31 43	mpcom	$⊢ (n + m \in ℕ_{0} \land (e trec (R) f \land (f trec (R) g \land (φ \land (e (R ↑_{r} n) f \land (n \in ℕ_{0} \land (f (R ↑_{r} m) g \land m \in ℕ_{0}))))))) \to (R ↑_{r} m) \circ (R ↑_{r} n) = R ↑_{r} (n + m)$
45		simprrl	$⊢ (f t*rec (R) g \land (φ \land (e (R ↑_{r} n) f \land (n \in ℕ_{0} \land (f (R ↑_{r} m) g \land m \in ℕ_{0}))))) \to e (R ↑_{r} n) f$
46	45	adantl	$⊢ (e trec (R) f \land (f trec (R) g \land (φ \land (e (R ↑_{r} n) f \land (n \in ℕ_{0} \land (f (R ↑_{r} m) g \land m \in ℕ_{0})))))) \to e (R ↑_{r} n) f$
47		simprrl	$⊢ (e (R ↑_{r} n) f \land (n \in ℕ_{0} \land (f (R ↑_{r} m) g \land m \in ℕ_{0}))) \to f (R ↑_{r} m) g$
48	47	adantl	$⊢ (φ \land (e (R ↑_{r} n) f \land (n \in ℕ_{0} \land (f (R ↑_{r} m) g \land m \in ℕ_{0})))) \to f (R ↑_{r} m) g$
49	48	adantl	$⊢ (f t*rec (R) g \land (φ \land (e (R ↑_{r} n) f \land (n \in ℕ_{0} \land (f (R ↑_{r} m) g \land m \in ℕ_{0}))))) \to f (R ↑_{r} m) g$
50	49	adantl	$⊢ (e trec (R) f \land (f trec (R) g \land (φ \land (e (R ↑_{r} n) f \land (n \in ℕ_{0} \land (f (R ↑_{r} m) g \land m \in ℕ_{0})))))) \to f (R ↑_{r} m) g$
51	50	adantl	$⊢ (n + m \in ℕ_{0} \land (e trec (R) f \land (f trec (R) g \land (φ \land (e (R ↑_{r} n) f \land (n \in ℕ_{0} \land (f (R ↑_{r} m) g \land m \in ℕ_{0}))))))) \to f (R ↑_{r} m) g$
52		vex	$⊢ f \in V$
53		breq2	$⊢ h = f \to (e (R ↑_{r} n) h \leftrightarrow e (R ↑_{r} n) f)$
54		breq1	$⊢ h = f \to (h (R ↑_{r} m) g \leftrightarrow f (R ↑_{r} m) g)$
55	53 54	anbi12d	$⊢ h = f \to ((e (R ↑_{r} n) h \land h (R ↑_{r} m) g) \leftrightarrow (e (R ↑_{r} n) f \land f (R ↑_{r} m) g))$
56	52 55	spcev	$⊢ (e (R ↑_{r} n) f \land f (R ↑_{r} m) g) \to \exists h (e (R ↑_{r} n) h \land h (R ↑_{r} m) g)$
57	46 51 56	syl2an2	$⊢ (n + m \in ℕ_{0} \land (e trec (R) f \land (f trec (R) g \land (φ \land (e (R ↑_{r} n) f \land (n \in ℕ_{0} \land (f (R ↑_{r} m) g \land m \in ℕ_{0}))))))) \to \exists h (e (R ↑_{r} n) h \land h (R ↑_{r} m) g)$
58		vex	$⊢ e \in V$
59		vex	$⊢ g \in V$
60	58 59	brco	$⊢ e ((R ↑_{r} m) \circ (R ↑_{r} n)) g \leftrightarrow \exists h (e (R ↑_{r} n) h \land h (R ↑_{r} m) g)$
61	57 60	sylibr	$⊢ (n + m \in ℕ_{0} \land (e trec (R) f \land (f trec (R) g \land (φ \land (e (R ↑_{r} n) f \land (n \in ℕ_{0} \land (f (R ↑_{r} m) g \land m \in ℕ_{0}))))))) \to e ((R ↑_{r} m) \circ (R ↑_{r} n)) g$
62	44 61	breqdi	$⊢ (n + m \in ℕ_{0} \land (e trec (R) f \land (f trec (R) g \land (φ \land (e (R ↑_{r} n) f \land (n \in ℕ_{0} \land (f (R ↑_{r} m) g \land m \in ℕ_{0}))))))) \to e (R ↑_{r} (n + m)) g$
63		oveq2	$⊢ i = n + m \to R ↑_{r} i = R ↑_{r} (n + m)$
64	63	breqd	$⊢ i = n + m \to (e (R ↑_{r} i) g \leftrightarrow e (R ↑_{r} (n + m)) g)$
65	64	rspcev	$⊢ (n + m \in ℕ_{0} \land e (R ↑_{r} (n + m)) g) \to \exists i \in ℕ_{0} e (R ↑_{r} i) g$
66	62 65	syldan	$⊢ (n + m \in ℕ_{0} \land (e trec (R) f \land (f trec (R) g \land (φ \land (e (R ↑_{r} n) f \land (n \in ℕ_{0} \land (f (R ↑_{r} m) g \land m \in ℕ_{0}))))))) \to \exists i \in ℕ_{0} e (R ↑_{r} i) g$
67	26 66	mpancom	$⊢ (e trec (R) f \land (f trec (R) g \land (φ \land (e (R ↑_{r} n) f \land (n \in ℕ_{0} \land (f (R ↑_{r} m) g \land m \in ℕ_{0})))))) \to \exists i \in ℕ_{0} e (R ↑_{r} i) g$
68		df-br	$⊢ e trec (R) g \leftrightarrow ⟨e, g⟩ \in trec (R)$
69	34 1	syl	$⊢ (e trec (R) f \land (f trec (R) g \land (φ \land (e (R ↑_{r} n) f \land (n \in ℕ_{0} \land (f (R ↑_{r} m) g \land m \in ℕ_{0})))))) \to Rel R$
70	69	dfrtrclrec2	$⊢ (e trec (R) f \land (f trec (R) g \land (φ \land (e (R ↑_{r} n) f \land (n \in ℕ_{0} \land (f (R ↑_{r} m) g \land m \in ℕ_{0})))))) \to (e t*rec (R) g \leftrightarrow \exists i \in ℕ_{0} e (R ↑_{r} i) g)$
71	68 70	bitr3id	$⊢ (e trec (R) f \land (f trec (R) g \land (φ \land (e (R ↑_{r} n) f \land (n \in ℕ_{0} \land (f (R ↑_{r} m) g \land m \in ℕ_{0})))))) \to (⟨e, g⟩ \in t*rec (R) \leftrightarrow \exists i \in ℕ_{0} e (R ↑_{r} i) g)$
72	67 71	mpbird	$⊢ (e trec (R) f \land (f trec (R) g \land (φ \land (e (R ↑_{r} n) f \land (n \in ℕ_{0} \land (f (R ↑_{r} m) g \land m \in ℕ_{0})))))) \to ⟨e, g⟩ \in t*rec (R)$
73	72	expcom	$⊢ (f trec (R) g \land (φ \land (e (R ↑_{r} n) f \land (n \in ℕ_{0} \land (f (R ↑_{r} m) g \land m \in ℕ_{0}))))) \to (e trec (R) f \to ⟨e, g⟩ \in t*rec (R))$
74	73	expcom	$⊢ (φ \land (e (R ↑_{r} n) f \land (n \in ℕ_{0} \land (f (R ↑_{r} m) g \land m \in ℕ_{0})))) \to (f trec (R) g \to (e trec (R) f \to ⟨e, g⟩ \in t*rec (R)))$
75	74	expcom	$⊢ (e (R ↑_{r} n) f \land (n \in ℕ_{0} \land (f (R ↑_{r} m) g \land m \in ℕ_{0}))) \to (φ \to (f trec (R) g \to (e trec (R) f \to ⟨e, g⟩ \in t*rec (R))))$
76	75	anassrs	$⊢ ((e (R ↑_{r} n) f \land n \in ℕ_{0}) \land (f (R ↑_{r} m) g \land m \in ℕ_{0})) \to (φ \to (f trec (R) g \to (e trec (R) f \to ⟨e, g⟩ \in t*rec (R))))$
77	76	impcom	$⊢ (φ \land ((e (R ↑_{r} n) f \land n \in ℕ_{0}) \land (f (R ↑_{r} m) g \land m \in ℕ_{0}))) \to (f trec (R) g \to (e trec (R) f \to ⟨e, g⟩ \in t*rec (R)))$
78	77	anassrs	$⊢ ((φ \land (e (R ↑_{r} n) f \land n \in ℕ_{0})) \land (f (R ↑_{r} m) g \land m \in ℕ_{0})) \to (f trec (R) g \to (e trec (R) f \to ⟨e, g⟩ \in t*rec (R)))$
79	78	impcom	$⊢ (f trec (R) g \land ((φ \land (e (R ↑_{r} n) f \land n \in ℕ_{0})) \land (f (R ↑_{r} m) g \land m \in ℕ_{0}))) \to (e trec (R) f \to ⟨e, g⟩ \in t*rec (R))$
80	79	anassrs	$⊢ ((f trec (R) g \land (φ \land (e (R ↑_{r} n) f \land n \in ℕ_{0}))) \land (f (R ↑_{r} m) g \land m \in ℕ_{0})) \to (e trec (R) f \to ⟨e, g⟩ \in t*rec (R))$
81	80	impcom	$⊢ (e trec (R) f \land ((f trec (R) g \land (φ \land (e (R ↑_{r} n) f \land n \in ℕ_{0}))) \land (f (R ↑_{r} m) g \land m \in ℕ_{0}))) \to ⟨e, g⟩ \in t*rec (R)$
82	81	anassrs	$⊢ ((e trec (R) f \land (f trec (R) g \land (φ \land (e (R ↑_{r} n) f \land n \in ℕ_{0})))) \land (f (R ↑_{r} m) g \land m \in ℕ_{0})) \to ⟨e, g⟩ \in t*rec (R)$
83	82	expcom	$⊢ (f (R ↑_{r} m) g \land m \in ℕ_{0}) \to ((e trec (R) f \land (f trec (R) g \land (φ \land (e (R ↑_{r} n) f \land n \in ℕ_{0})))) \to ⟨e, g⟩ \in t*rec (R))$
84	83	expcom	$⊢ m \in ℕ_{0} \to (f (R ↑_{r} m) g \to ((e trec (R) f \land (f trec (R) g \land (φ \land (e (R ↑_{r} n) f \land n \in ℕ_{0})))) \to ⟨e, g⟩ \in t*rec (R)))$
85	84	rexlimiv	$⊢ \exists m \in ℕ_{0} f (R ↑_{r} m) g \to ((e trec (R) f \land (f trec (R) g \land (φ \land (e (R ↑_{r} n) f \land n \in ℕ_{0})))) \to ⟨e, g⟩ \in t*rec (R))$
86	17 85	mpcom	$⊢ (e trec (R) f \land (f trec (R) g \land (φ \land (e (R ↑_{r} n) f \land n \in ℕ_{0})))) \to ⟨e, g⟩ \in t*rec (R)$
87	86	expcom	$⊢ (f trec (R) g \land (φ \land (e (R ↑_{r} n) f \land n \in ℕ_{0}))) \to (e trec (R) f \to ⟨e, g⟩ \in t*rec (R))$
88	87	anassrs	$⊢ ((f trec (R) g \land φ) \land (e (R ↑_{r} n) f \land n \in ℕ_{0})) \to (e trec (R) f \to ⟨e, g⟩ \in t*rec (R))$
89	88	impcom	$⊢ (e trec (R) f \land ((f trec (R) g \land φ) \land (e (R ↑_{r} n) f \land n \in ℕ_{0}))) \to ⟨e, g⟩ \in t*rec (R)$
90	89	anassrs	$⊢ ((e trec (R) f \land (f trec (R) g \land φ)) \land (e (R ↑_{r} n) f \land n \in ℕ_{0})) \to ⟨e, g⟩ \in t*rec (R)$
91	90	expcom	$⊢ (e (R ↑_{r} n) f \land n \in ℕ_{0}) \to ((e trec (R) f \land (f trec (R) g \land φ)) \to ⟨e, g⟩ \in t*rec (R))$
92	91	expcom	$⊢ n \in ℕ_{0} \to (e (R ↑_{r} n) f \to ((e trec (R) f \land (f trec (R) g \land φ)) \to ⟨e, g⟩ \in t*rec (R)))$
93	92	rexlimiv	$⊢ \exists n \in ℕ_{0} e (R ↑_{r} n) f \to ((e trec (R) f \land (f trec (R) g \land φ)) \to ⟨e, g⟩ \in t*rec (R))$
94	12 93	mpcom	$⊢ (e trec (R) f \land (f trec (R) g \land φ)) \to ⟨e, g⟩ \in t*rec (R)$
95	94	anassrs	$⊢ ((e trec (R) f \land f trec (R) g) \land φ) \to ⟨e, g⟩ \in t*rec (R)$
96	95	expcom	$⊢ φ \to ((e trec (R) f \land f trec (R) g) \to ⟨e, g⟩ \in t*rec (R))$
97	96	exlimdv	$⊢ φ \to (\exists f (e trec (R) f \land f trec (R) g) \to ⟨e, g⟩ \in t*rec (R))$
98	6 7 97	sylc	$⊢ (⟨e, g⟩ = ⟨e, g⟩ \land (\exists f (e trec (R) f \land f trec (R) g) \land φ)) \to ⟨e, g⟩ \in t*rec (R)$
99		eleq1	$⊢ d = ⟨e, g⟩ \to (d \in trec (R) \leftrightarrow ⟨e, g⟩ \in trec (R))$
100	98 99	imbitrrid	$⊢ d = ⟨e, g⟩ \to ((⟨e, g⟩ = ⟨e, g⟩ \land (\exists f (e trec (R) f \land f trec (R) g) \land φ)) \to d \in t*rec (R))$
101	5 100	sylbid	$⊢ d = ⟨e, g⟩ \to ((d = ⟨e, g⟩ \land (\exists f (e trec (R) f \land f trec (R) g) \land φ)) \to d \in t*rec (R))$
102	101	anabsi5	$⊢ (d = ⟨e, g⟩ \land (\exists f (e trec (R) f \land f trec (R) g) \land φ)) \to d \in t*rec (R)$
103	102	anassrs	$⊢ ((d = ⟨e, g⟩ \land \exists f (e trec (R) f \land f trec (R) g)) \land φ) \to d \in t*rec (R)$
104	103	expcom	$⊢ φ \to ((d = ⟨e, g⟩ \land \exists f (e trec (R) f \land f trec (R) g)) \to d \in t*rec (R))$
105	104	exlimdvv	$⊢ φ \to (\exists e \exists g (d = ⟨e, g⟩ \land \exists f (e trec (R) f \land f trec (R) g)) \to d \in t*rec (R))$
106	3 105	biimtrid	$⊢ φ \to (d \in \{⟨e, g⟩ \| \exists f (e trec (R) f \land f trec (R) g)\} \to d \in t*rec (R))$
107		eleq2	$⊢ trec (R) \circ trec (R) = \{⟨e, g⟩ \| \exists f (e trec (R) f \land f trec (R) g)\} \to (d \in (trec (R) \circ trec (R)) \leftrightarrow d \in \{⟨e, g⟩ \| \exists f (e trec (R) f \land f trec (R) g)\})$
108	107	imbi1d	$⊢ trec (R) \circ trec (R) = \{⟨e, g⟩ \| \exists f (e trec (R) f \land f trec (R) g)\} \to ((d \in (trec (R) \circ trec (R)) \to d \in trec (R)) \leftrightarrow (d \in \{⟨e, g⟩ \| \exists f (e trec (R) f \land f trec (R) g)\} \to d \in trec (R)))$
109	106 108	imbitrrid	$⊢ trec (R) \circ trec (R) = \{⟨e, g⟩ \| \exists f (e trec (R) f \land f trec (R) g)\} \to (φ \to (d \in (trec (R) \circ trec (R)) \to d \in t*rec (R)))$
110	2 109	ax-mp	$⊢ φ \to (d \in (trec (R) \circ trec (R)) \to d \in t*rec (R))$
111	110	ssrdv	$⊢ φ \to trec (R) \circ trec (R) \subseteq t*rec (R)$

Metamath Proof Explorer

Theorem rtrclreclem3

Proof