dfrtrclrec2

Description: If two elements are connected by a reflexive, transitive closure, then they are connected via n instances the relation, for some n . (Contributed by Drahflow, 12-Nov-2015) (Revised by AV, 13-Jul-2024)

		Ref	Expression
	Hypothesis	dfrtrclrec2.1	$⊢ φ \to Rel R$
	Assertion	dfrtrclrec2	$⊢ φ \to (A t*rec (R) B \leftrightarrow \exists n \in ℕ_{0} A (R ↑_{r} n) B)$

Proof

Step	Hyp	Ref	Expression
1		dfrtrclrec2.1	$⊢ φ \to Rel R$
2		simpr	$⊢ (φ \land R \in V) \to R \in V$
3		nn0ex	$⊢ ℕ_{0} \in V$
4		ovex	$⊢ R ↑_{r} n \in V$
5	3 4	iunex	$⊢ ⋃_{n \in ℕ_{0}} (R ↑_{r} n) \in V$
6		oveq1	$⊢ r = R \to r ↑_{r} n = R ↑_{r} n$
7	6	iuneq2d	$⊢ r = R \to ⋃_{n \in ℕ_{0}} (r ↑_{r} n) = ⋃_{n \in ℕ_{0}} (R ↑_{r} n)$
8		eqid	$⊢ (r \in V ⟼ ⋃_{n \in ℕ_{0}} (r ↑_{r} n)) = (r \in V ⟼ ⋃_{n \in ℕ_{0}} (r ↑_{r} n))$
9	7 8	fvmptg	$⊢ (R \in V \land ⋃_{n \in ℕ_{0}} (R ↑_{r} n) \in V) \to (r \in V ⟼ ⋃_{n \in ℕ_{0}} (r ↑_{r} n)) (R) = ⋃_{n \in ℕ_{0}} (R ↑_{r} n)$
10	2 5 9	sylancl	$⊢ (φ \land R \in V) \to (r \in V ⟼ ⋃_{n \in ℕ_{0}} (r ↑_{r} n)) (R) = ⋃_{n \in ℕ_{0}} (R ↑_{r} n)$
11	10	ex	$⊢ φ \to (R \in V \to (r \in V ⟼ ⋃_{n \in ℕ_{0}} (r ↑_{r} n)) (R) = ⋃_{n \in ℕ_{0}} (R ↑_{r} n))$
12		iun0	$⊢ ⋃_{n \in ℕ_{0}} \emptyset = \emptyset$
13	12	a1i	$⊢ \neg R \in V \to ⋃_{n \in ℕ_{0}} \emptyset = \emptyset$
14		reldmrelexp	$⊢ Rel dom ↑_{r}$
15	14	ovprc1	$⊢ \neg R \in V \to R ↑_{r} n = \emptyset$
16	15	iuneq2d	$⊢ \neg R \in V \to ⋃_{n \in ℕ_{0}} (R ↑_{r} n) = ⋃_{n \in ℕ_{0}} \emptyset$
17		fvprc	$⊢ \neg R \in V \to (r \in V ⟼ ⋃_{n \in ℕ_{0}} (r ↑_{r} n)) (R) = \emptyset$
18	13 16 17	3eqtr4rd	$⊢ \neg R \in V \to (r \in V ⟼ ⋃_{n \in ℕ_{0}} (r ↑_{r} n)) (R) = ⋃_{n \in ℕ_{0}} (R ↑_{r} n)$
19	11 18	pm2.61d1	$⊢ φ \to (r \in V ⟼ ⋃_{n \in ℕ_{0}} (r ↑_{r} n)) (R) = ⋃_{n \in ℕ_{0}} (R ↑_{r} n)$
20		breq	$⊢ (r \in V ⟼ ⋃_{n \in ℕ_{0}} (r ↑_{r} n)) (R) = ⋃_{n \in ℕ_{0}} (R ↑_{r} n) \to (A (r \in V ⟼ ⋃_{n \in ℕ_{0}} (r ↑_{r} n)) (R) B \leftrightarrow A ⋃_{n \in ℕ_{0}} (R ↑_{r} n) B)$
21		eliun	$⊢ ⟨A, B⟩ \in ⋃_{n \in ℕ_{0}} (R ↑_{r} n) \leftrightarrow \exists n \in ℕ_{0} ⟨A, B⟩ \in (R ↑_{r} n)$
22	21	a1i	$⊢ φ \to (⟨A, B⟩ \in ⋃_{n \in ℕ_{0}} (R ↑_{r} n) \leftrightarrow \exists n \in ℕ_{0} ⟨A, B⟩ \in (R ↑_{r} n))$
23		df-br	$⊢ A ⋃_{n \in ℕ_{0}} (R ↑_{r} n) B \leftrightarrow ⟨A, B⟩ \in ⋃_{n \in ℕ_{0}} (R ↑_{r} n)$
24		df-br	$⊢ A (R ↑_{r} n) B \leftrightarrow ⟨A, B⟩ \in (R ↑_{r} n)$
25	24	rexbii	$⊢ \exists n \in ℕ_{0} A (R ↑_{r} n) B \leftrightarrow \exists n \in ℕ_{0} ⟨A, B⟩ \in (R ↑_{r} n)$
26	22 23 25	3bitr4g	$⊢ φ \to (A ⋃_{n \in ℕ_{0}} (R ↑_{r} n) B \leftrightarrow \exists n \in ℕ_{0} A (R ↑_{r} n) B)$
27	20 26	sylan9bb	$⊢ ((r \in V ⟼ ⋃_{n \in ℕ_{0}} (r ↑_{r} n)) (R) = ⋃_{n \in ℕ_{0}} (R ↑_{r} n) \land φ) \to (A (r \in V ⟼ ⋃_{n \in ℕ_{0}} (r ↑_{r} n)) (R) B \leftrightarrow \exists n \in ℕ_{0} A (R ↑_{r} n) B)$
28	19 27	mpancom	$⊢ φ \to (A (r \in V ⟼ ⋃_{n \in ℕ_{0}} (r ↑_{r} n)) (R) B \leftrightarrow \exists n \in ℕ_{0} A (R ↑_{r} n) B)$
29		df-rtrclrec	$⊢ t*rec = (r \in V ⟼ ⋃_{n \in ℕ_{0}} (r ↑_{r} n))$
30		fveq1	$⊢ trec = (r \in V ⟼ ⋃_{n \in ℕ_{0}} (r ↑_{r} n)) \to trec (R) = (r \in V ⟼ ⋃_{n \in ℕ_{0}} (r ↑_{r} n)) (R)$
31	30	breqd	$⊢ trec = (r \in V ⟼ ⋃_{n \in ℕ_{0}} (r ↑_{r} n)) \to (A trec (R) B \leftrightarrow A (r \in V ⟼ ⋃_{n \in ℕ_{0}} (r ↑_{r} n)) (R) B)$
32	31	bibi1d	$⊢ trec = (r \in V ⟼ ⋃_{n \in ℕ_{0}} (r ↑_{r} n)) \to ((A trec (R) B \leftrightarrow \exists n \in ℕ_{0} A (R ↑_{r} n) B) \leftrightarrow (A (r \in V ⟼ ⋃_{n \in ℕ_{0}} (r ↑_{r} n)) (R) B \leftrightarrow \exists n \in ℕ_{0} A (R ↑_{r} n) B))$
33	32	imbi2d	$⊢ trec = (r \in V ⟼ ⋃_{n \in ℕ_{0}} (r ↑_{r} n)) \to ((φ \to (A trec (R) B \leftrightarrow \exists n \in ℕ_{0} A (R ↑_{r} n) B)) \leftrightarrow (φ \to (A (r \in V ⟼ ⋃_{n \in ℕ_{0}} (r ↑_{r} n)) (R) B \leftrightarrow \exists n \in ℕ_{0} A (R ↑_{r} n) B)))$
34	29 33	ax-mp	$⊢ (φ \to (A t*rec (R) B \leftrightarrow \exists n \in ℕ_{0} A (R ↑_{r} n) B)) \leftrightarrow (φ \to (A (r \in V ⟼ ⋃_{n \in ℕ_{0}} (r ↑_{r} n)) (R) B \leftrightarrow \exists n \in ℕ_{0} A (R ↑_{r} n) B))$
35	28 34	mpbir	$⊢ φ \to (A t*rec (R) B \leftrightarrow \exists n \in ℕ_{0} A (R ↑_{r} n) B)$

Metamath Proof Explorer

Theorem dfrtrclrec2

Proof