This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem brtxpsd

Description: Expansion of a common form used in quantifier-free definitions. (Contributed by Scott Fenton, 17-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Hypotheses brtxpsd.1 ⊢ 𝐴 ∈ V
brtxpsd.2 ⊢ 𝐵 ∈ V
Assertion brtxpsd ( ¬ 𝐴 ran ( ( V ⊗ E ) △ ( 𝑅 ⊗ V ) ) 𝐵 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐵 ↔ 𝑥 𝑅 𝐴 ) )

Proof

Step Hyp Ref Expression
1 brtxpsd.1 ⊢ 𝐴 ∈ V
2 brtxpsd.2 ⊢ 𝐵 ∈ V
3 df-br ⊢ ( 𝐴 ran ( ( V ⊗ E ) △ ( 𝑅 ⊗ V ) ) 𝐵 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ ran ( ( V ⊗ E ) △ ( 𝑅 ⊗ V ) ) )
4 opex ⊢ ⟨ 𝐴 , 𝐵 ⟩ ∈ V
5 4 elrn ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ran ( ( V ⊗ E ) △ ( 𝑅 ⊗ V ) ) ↔ ∃ 𝑥 𝑥 ( ( V ⊗ E ) △ ( 𝑅 ⊗ V ) ) ⟨ 𝐴 , 𝐵 ⟩ )
6 brsymdif ⊢ ( 𝑥 ( ( V ⊗ E ) △ ( 𝑅 ⊗ V ) ) ⟨ 𝐴 , 𝐵 ⟩ ↔ ¬ ( 𝑥 ( V ⊗ E ) ⟨ 𝐴 , 𝐵 ⟩ ↔ 𝑥 ( 𝑅 ⊗ V ) ⟨ 𝐴 , 𝐵 ⟩ ) )
7 brv ⊢ 𝑥 V 𝐴
8 vex ⊢ 𝑥 ∈ V
9 8 1 2 brtxp ⊢ ( 𝑥 ( V ⊗ E ) ⟨ 𝐴 , 𝐵 ⟩ ↔ ( 𝑥 V 𝐴 ∧ 𝑥 E 𝐵 ) )
10 7 9 mpbiran ⊢ ( 𝑥 ( V ⊗ E ) ⟨ 𝐴 , 𝐵 ⟩ ↔ 𝑥 E 𝐵 )
11 2 epeli ⊢ ( 𝑥 E 𝐵 ↔ 𝑥 ∈ 𝐵 )
12 10 11 bitri ⊢ ( 𝑥 ( V ⊗ E ) ⟨ 𝐴 , 𝐵 ⟩ ↔ 𝑥 ∈ 𝐵 )
13 brv ⊢ 𝑥 V 𝐵
14 8 1 2 brtxp ⊢ ( 𝑥 ( 𝑅 ⊗ V ) ⟨ 𝐴 , 𝐵 ⟩ ↔ ( 𝑥 𝑅 𝐴 ∧ 𝑥 V 𝐵 ) )
15 13 14 mpbiran2 ⊢ ( 𝑥 ( 𝑅 ⊗ V ) ⟨ 𝐴 , 𝐵 ⟩ ↔ 𝑥 𝑅 𝐴 )
16 12 15 bibi12i ⊢ ( ( 𝑥 ( V ⊗ E ) ⟨ 𝐴 , 𝐵 ⟩ ↔ 𝑥 ( 𝑅 ⊗ V ) ⟨ 𝐴 , 𝐵 ⟩ ) ↔ ( 𝑥 ∈ 𝐵 ↔ 𝑥 𝑅 𝐴 ) )
17 6 16 xchbinx ⊢ ( 𝑥 ( ( V ⊗ E ) △ ( 𝑅 ⊗ V ) ) ⟨ 𝐴 , 𝐵 ⟩ ↔ ¬ ( 𝑥 ∈ 𝐵 ↔ 𝑥 𝑅 𝐴 ) )
18 17 exbii ⊢ ( ∃ 𝑥 𝑥 ( ( V ⊗ E ) △ ( 𝑅 ⊗ V ) ) ⟨ 𝐴 , 𝐵 ⟩ ↔ ∃ 𝑥 ¬ ( 𝑥 ∈ 𝐵 ↔ 𝑥 𝑅 𝐴 ) )
19 5 18 bitri ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ran ( ( V ⊗ E ) △ ( 𝑅 ⊗ V ) ) ↔ ∃ 𝑥 ¬ ( 𝑥 ∈ 𝐵 ↔ 𝑥 𝑅 𝐴 ) )
20 exnal ⊢ ( ∃ 𝑥 ¬ ( 𝑥 ∈ 𝐵 ↔ 𝑥 𝑅 𝐴 ) ↔ ¬ ∀ 𝑥 ( 𝑥 ∈ 𝐵 ↔ 𝑥 𝑅 𝐴 ) )
21 3 19 20 3bitrri ⊢ ( ¬ ∀ 𝑥 ( 𝑥 ∈ 𝐵 ↔ 𝑥 𝑅 𝐴 ) ↔ 𝐴 ran ( ( V ⊗ E ) △ ( 𝑅 ⊗ V ) ) 𝐵 )
22 21 con1bii ⊢ ( ¬ 𝐴 ran ( ( V ⊗ E ) △ ( 𝑅 ⊗ V ) ) 𝐵 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐵 ↔ 𝑥 𝑅 𝐴 ) )