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 𝑅 ∧ 𝐴 ∈ [ 𝑥 ] 𝑅 ) → [ 𝑥 ] 𝑅 = [ 𝐴 ] ≀ 𝑅 ) ) )