Theorem 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	⊢ ( 𝜑 → Rel 𝑅 )
Assertion	dfrtrclrec2	⊢ ( 𝜑 → ( 𝐴 ( t*rec ‘ 𝑅 ) 𝐵 ↔ ∃ 𝑛 ∈ ℕ0 𝐴 ( 𝑅 ↑𝑟 𝑛 ) 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		dfrtrclrec2.1	⊢ ( 𝜑 → Rel 𝑅 )
2		simpr	⊢ ( ( 𝜑 ∧ 𝑅 ∈ V ) → 𝑅 ∈ V )
3		nn0ex	⊢ ℕ0 ∈ V
4		ovex	⊢ ( 𝑅 ↑𝑟 𝑛 ) ∈ V
5	3 4	iunex	⊢ ∪ 𝑛 ∈ ℕ0 ( 𝑅 ↑𝑟 𝑛 ) ∈ V
6		oveq1	⊢ ( 𝑟 = 𝑅 → ( 𝑟 ↑𝑟 𝑛 ) = ( 𝑅 ↑𝑟 𝑛 ) )
7	6	iuneq2d	⊢ ( 𝑟 = 𝑅 → ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) = ∪ 𝑛 ∈ ℕ0 ( 𝑅 ↑𝑟 𝑛 ) )
8		eqid	⊢ ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) ) = ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) )
9	7 8	fvmptg	⊢ ( ( 𝑅 ∈ V ∧ ∪ 𝑛 ∈ ℕ0 ( 𝑅 ↑𝑟 𝑛 ) ∈ V ) → ( ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) ) ‘ 𝑅 ) = ∪ 𝑛 ∈ ℕ0 ( 𝑅 ↑𝑟 𝑛 ) )
10	2 5 9	sylancl	⊢ ( ( 𝜑 ∧ 𝑅 ∈ V ) → ( ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) ) ‘ 𝑅 ) = ∪ 𝑛 ∈ ℕ0 ( 𝑅 ↑𝑟 𝑛 ) )
11	10	ex	⊢ ( 𝜑 → ( 𝑅 ∈ V → ( ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) ) ‘ 𝑅 ) = ∪ 𝑛 ∈ ℕ0 ( 𝑅 ↑𝑟 𝑛 ) ) )
12		iun0	⊢ ∪ 𝑛 ∈ ℕ0 ∅ = ∅
13	12	a1i	⊢ ( ¬ 𝑅 ∈ V → ∪ 𝑛 ∈ ℕ0 ∅ = ∅ )
14		reldmrelexp	⊢ Rel dom ↑𝑟
15	14	ovprc1	⊢ ( ¬ 𝑅 ∈ V → ( 𝑅 ↑𝑟 𝑛 ) = ∅ )
16	15	iuneq2d	⊢ ( ¬ 𝑅 ∈ V → ∪ 𝑛 ∈ ℕ0 ( 𝑅 ↑𝑟 𝑛 ) = ∪ 𝑛 ∈ ℕ0 ∅ )
17		fvprc	⊢ ( ¬ 𝑅 ∈ V → ( ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) ) ‘ 𝑅 ) = ∅ )
18	13 16 17	3eqtr4rd	⊢ ( ¬ 𝑅 ∈ V → ( ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) ) ‘ 𝑅 ) = ∪ 𝑛 ∈ ℕ0 ( 𝑅 ↑𝑟 𝑛 ) )
19	11 18	pm2.61d1	⊢ ( 𝜑 → ( ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) ) ‘ 𝑅 ) = ∪ 𝑛 ∈ ℕ0 ( 𝑅 ↑𝑟 𝑛 ) )
20		breq	⊢ ( ( ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) ) ‘ 𝑅 ) = ∪ 𝑛 ∈ ℕ0 ( 𝑅 ↑𝑟 𝑛 ) → ( 𝐴 ( ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) ) ‘ 𝑅 ) 𝐵 ↔ 𝐴 ∪ 𝑛 ∈ ℕ0 ( 𝑅 ↑𝑟 𝑛 ) 𝐵 ) )
21		eliun	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ∪ 𝑛 ∈ ℕ0 ( 𝑅 ↑𝑟 𝑛 ) ↔ ∃ 𝑛 ∈ ℕ0 ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑅 ↑𝑟 𝑛 ) )
22	21	a1i	⊢ ( 𝜑 → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ∪ 𝑛 ∈ ℕ0 ( 𝑅 ↑𝑟 𝑛 ) ↔ ∃ 𝑛 ∈ ℕ0 ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑅 ↑𝑟 𝑛 ) ) )
23		df-br	⊢ ( 𝐴 ∪ 𝑛 ∈ ℕ0 ( 𝑅 ↑𝑟 𝑛 ) 𝐵 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ ∪ 𝑛 ∈ ℕ0 ( 𝑅 ↑𝑟 𝑛 ) )
24		df-br	⊢ ( 𝐴 ( 𝑅 ↑𝑟 𝑛 ) 𝐵 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑅 ↑𝑟 𝑛 ) )
25	24	rexbii	⊢ ( ∃ 𝑛 ∈ ℕ0 𝐴 ( 𝑅 ↑𝑟 𝑛 ) 𝐵 ↔ ∃ 𝑛 ∈ ℕ0 ⟨ 𝐴 , 𝐵 ⟩ ∈ ( 𝑅 ↑𝑟 𝑛 ) )
26	22 23 25	3bitr4g	⊢ ( 𝜑 → ( 𝐴 ∪ 𝑛 ∈ ℕ0 ( 𝑅 ↑𝑟 𝑛 ) 𝐵 ↔ ∃ 𝑛 ∈ ℕ0 𝐴 ( 𝑅 ↑𝑟 𝑛 ) 𝐵 ) )
27	20 26	sylan9bb	⊢ ( ( ( ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) ) ‘ 𝑅 ) = ∪ 𝑛 ∈ ℕ0 ( 𝑅 ↑𝑟 𝑛 ) ∧ 𝜑 ) → ( 𝐴 ( ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) ) ‘ 𝑅 ) 𝐵 ↔ ∃ 𝑛 ∈ ℕ0 𝐴 ( 𝑅 ↑𝑟 𝑛 ) 𝐵 ) )
28	19 27	mpancom	⊢ ( 𝜑 → ( 𝐴 ( ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) ) ‘ 𝑅 ) 𝐵 ↔ ∃ 𝑛 ∈ ℕ0 𝐴 ( 𝑅 ↑𝑟 𝑛 ) 𝐵 ) )
29		df-rtrclrec	⊢ t*rec = ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) )
30		fveq1	⊢ ( t*rec = ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) ) → ( t*rec ‘ 𝑅 ) = ( ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) ) ‘ 𝑅 ) )
31	30	breqd	⊢ ( t*rec = ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) ) → ( 𝐴 ( t*rec ‘ 𝑅 ) 𝐵 ↔ 𝐴 ( ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) ) ‘ 𝑅 ) 𝐵 ) )
32	31	bibi1d	⊢ ( t*rec = ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) ) → ( ( 𝐴 ( t*rec ‘ 𝑅 ) 𝐵 ↔ ∃ 𝑛 ∈ ℕ0 𝐴 ( 𝑅 ↑𝑟 𝑛 ) 𝐵 ) ↔ ( 𝐴 ( ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) ) ‘ 𝑅 ) 𝐵 ↔ ∃ 𝑛 ∈ ℕ0 𝐴 ( 𝑅 ↑𝑟 𝑛 ) 𝐵 ) ) )
33	32	imbi2d	⊢ ( t*rec = ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) ) → ( ( 𝜑 → ( 𝐴 ( t*rec ‘ 𝑅 ) 𝐵 ↔ ∃ 𝑛 ∈ ℕ0 𝐴 ( 𝑅 ↑𝑟 𝑛 ) 𝐵 ) ) ↔ ( 𝜑 → ( 𝐴 ( ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) ) ‘ 𝑅 ) 𝐵 ↔ ∃ 𝑛 ∈ ℕ0 𝐴 ( 𝑅 ↑𝑟 𝑛 ) 𝐵 ) ) ) )
34	29 33	ax-mp	⊢ ( ( 𝜑 → ( 𝐴 ( t*rec ‘ 𝑅 ) 𝐵 ↔ ∃ 𝑛 ∈ ℕ0 𝐴 ( 𝑅 ↑𝑟 𝑛 ) 𝐵 ) ) ↔ ( 𝜑 → ( 𝐴 ( ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) ) ‘ 𝑅 ) 𝐵 ↔ ∃ 𝑛 ∈ ℕ0 𝐴 ( 𝑅 ↑𝑟 𝑛 ) 𝐵 ) ) )
35	28 34	mpbir	⊢ ( 𝜑 → ( 𝐴 ( t*rec ‘ 𝑅 ) 𝐵 ↔ ∃ 𝑛 ∈ ℕ0 𝐴 ( 𝑅 ↑𝑟 𝑛 ) 𝐵 ) )