Metamath Proof Explorer

Theorem brfvrcld

Description: If two elements are connected by the reflexive closure of a relation, then they are connected via zero or one instances the relation. (Contributed by RP, 21-Jul-2020)

Ref Expression
Hypothesis brfvrcld.r ⊢ φ → R ∈ V
Assertion brfvrcld ⊢ φ → A r* ⁡ R B ↔ A R ↑ r 0 B ∨ A R ↑ r 1 B

Proof

Step Hyp Ref Expression
1 brfvrcld.r ⊢ φ → R ∈ V
2 dfrcl4 ⊢ r* = r ∈ V ⟼ ⋃ n ∈ 0 1 r ↑ r n
3 0nn0 ⊢ 0 ∈ ℕ 0
4 1nn0 ⊢ 1 ∈ ℕ 0
5 prssi ⊢ 0 ∈ ℕ 0 ∧ 1 ∈ ℕ 0 → 0 1 ⊆ ℕ 0
6 3 4 5 mp2an ⊢ 0 1 ⊆ ℕ 0
7 6 a1i ⊢ φ → 0 1 ⊆ ℕ 0
8 2 1 7 brmptiunrelexpd ⊢ φ → A r* ⁡ R B ↔ ∃ n ∈ 0 1 A R ↑ r n B
9 oveq2 ⊢ n = 0 → R ↑ r n = R ↑ r 0
10 9 breqd ⊢ n = 0 → A R ↑ r n B ↔ A R ↑ r 0 B
11 oveq2 ⊢ n = 1 → R ↑ r n = R ↑ r 1
12 11 breqd ⊢ n = 1 → A R ↑ r n B ↔ A R ↑ r 1 B
13 10 12 rexprg ⊢ 0 ∈ ℕ 0 ∧ 1 ∈ ℕ 0 → ∃ n ∈ 0 1 A R ↑ r n B ↔ A R ↑ r 0 B ∨ A R ↑ r 1 B
14 3 4 13 mp2an ⊢ ∃ n ∈ 0 1 A R ↑ r n B ↔ A R ↑ r 0 B ∨ A R ↑ r 1 B
15 8 14 bitrdi ⊢ φ → A r* ⁡ R B ↔ A R ↑ r 0 B ∨ A R ↑ r 1 B