Metamath Proof Explorer

Theorem brmptiunrelexpd

Description: If two elements are connected by an indexed union of relational powers, then they are connected via n instances the relation, for some n . Generalization of dfrtrclrec2 . (Contributed by RP, 21-Jul-2020)

Ref Expression
Hypotheses brmptiunrelexpd.c ⊢ C = r ∈ V ⟼ ⋃ n ∈ N r ↑ r n
brmptiunrelexpd.r ⊢ φ → R ∈ V
brmptiunrelexpd.n ⊢ φ → N ⊆ ℕ 0
Assertion brmptiunrelexpd ⊢ φ → A C ⁡ R B ↔ ∃ n ∈ N A R ↑ r n B

Proof

Step Hyp Ref Expression
1 brmptiunrelexpd.c ⊢ C = r ∈ V ⟼ ⋃ n ∈ N r ↑ r n
2 brmptiunrelexpd.r ⊢ φ → R ∈ V
3 brmptiunrelexpd.n ⊢ φ → N ⊆ ℕ 0
4 nn0ex ⊢ ℕ 0 ∈ V
5 4 ssex ⊢ N ⊆ ℕ 0 → N ∈ V
6 3 5 syl ⊢ φ → N ∈ V
7 1 briunov2 ⊢ R ∈ V ∧ N ∈ V → A C ⁡ R B ↔ ∃ n ∈ N A R ↑ r n B
8 2 6 7 syl2anc ⊢ φ → A C ⁡ R B ↔ ∃ n ∈ N A R ↑ r n B