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

Metamath Proof Explorer

Theorem disjlem19

Description: Lemma for disjdmqseq , partim2 and petlem via disjdmqs , (general version of the former prtlem19 ). (Contributed by Peter Mazsa, 16-Sep-2021)

Ref Expression
Assertion disjlem19 ( 𝐴 ∈ 𝑉 → ( Disj 𝑅 → ( ( 𝑥 ∈ dom 𝑅 ∧ 𝐴 ∈ [ 𝑥 ] 𝑅 ) → [ 𝑥 ] 𝑅 = [ 𝐴 ] ≀ 𝑅 ) ) )

Proof

Step Hyp Ref Expression
1 disjlem18 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑧 ∈ V ) → ( Disj 𝑅 → ( ( 𝑥 ∈ dom 𝑅 ∧ 𝐴 ∈ [ 𝑥 ] 𝑅 ) → ( 𝑧 ∈ [ 𝑥 ] 𝑅 ↔ 𝐴 ≀ 𝑅 𝑧 ) ) ) )
2 1 elvd ⊢ ( 𝐴 ∈ 𝑉 → ( Disj 𝑅 → ( ( 𝑥 ∈ dom 𝑅 ∧ 𝐴 ∈ [ 𝑥 ] 𝑅 ) → ( 𝑧 ∈ [ 𝑥 ] 𝑅 ↔ 𝐴 ≀ 𝑅 𝑧 ) ) ) )
3 2 imp31 ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ Disj 𝑅 ) ∧ ( 𝑥 ∈ dom 𝑅 ∧ 𝐴 ∈ [ 𝑥 ] 𝑅 ) ) → ( 𝑧 ∈ [ 𝑥 ] 𝑅 ↔ 𝐴 ≀ 𝑅 𝑧 ) )
4 elecALTV ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑧 ∈ V ) → ( 𝑧 ∈ [ 𝐴 ] ≀ 𝑅 ↔ 𝐴 ≀ 𝑅 𝑧 ) )
5 4 elvd ⊢ ( 𝐴 ∈ 𝑉 → ( 𝑧 ∈ [ 𝐴 ] ≀ 𝑅 ↔ 𝐴 ≀ 𝑅 𝑧 ) )
6 5 ad2antrr ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ Disj 𝑅 ) ∧ ( 𝑥 ∈ dom 𝑅 ∧ 𝐴 ∈ [ 𝑥 ] 𝑅 ) ) → ( 𝑧 ∈ [ 𝐴 ] ≀ 𝑅 ↔ 𝐴 ≀ 𝑅 𝑧 ) )
7 3 6 bitr4d ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ Disj 𝑅 ) ∧ ( 𝑥 ∈ dom 𝑅 ∧ 𝐴 ∈ [ 𝑥 ] 𝑅 ) ) → ( 𝑧 ∈ [ 𝑥 ] 𝑅 ↔ 𝑧 ∈ [ 𝐴 ] ≀ 𝑅 ) )
8 7 eqrdv ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ Disj 𝑅 ) ∧ ( 𝑥 ∈ dom 𝑅 ∧ 𝐴 ∈ [ 𝑥 ] 𝑅 ) ) → [ 𝑥 ] 𝑅 = [ 𝐴 ] ≀ 𝑅 )
9 8 exp31 ⊢ ( 𝐴 ∈ 𝑉 → ( Disj 𝑅 → ( ( 𝑥 ∈ dom 𝑅 ∧ 𝐴 ∈ [ 𝑥 ] 𝑅 ) → [ 𝑥 ] 𝑅 = [ 𝐴 ] ≀ 𝑅 ) ) )