rtrclreclem3

Description: The reflexive, transitive closure is indeed transitive. (Contributed by Drahflow, 12-Nov-2015) (Revised by RP, 30-May-2020)

	Ref	Expression
Hypotheses	rtrclreclem.rel	$⊢ φ \to Rel R$
	rtrclreclem.rex	$⊢ φ \to R \in V$
Assertion	rtrclreclem3	$⊢ φ \to trec (R) \circ trec (R) \subseteq t*rec (R)$

Proof

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

Metamath Proof Explorer

Theorem rtrclreclem3

Proof