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

Metamath Proof Explorer

Theorem disjlem17

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

Ref Expression
Assertion disjlem17 ( Disj 𝑅 → ( ( 𝑥 ∈ dom 𝑅 ∧ 𝐴 ∈ [ 𝑥 ] 𝑅 ) → ( ∃ 𝑦 ∈ dom 𝑅 ( 𝐴 ∈ [ 𝑦 ] 𝑅 ∧ 𝐵 ∈ [ 𝑦 ] 𝑅 ) → 𝐵 ∈ [ 𝑥 ] 𝑅 ) ) )

Proof

Step Hyp Ref Expression
1 df-rex ⊢ ( ∃ 𝑦 ∈ dom 𝑅 ( 𝐴 ∈ [ 𝑦 ] 𝑅 ∧ 𝐵 ∈ [ 𝑦 ] 𝑅 ) ↔ ∃ 𝑦 ( 𝑦 ∈ dom 𝑅 ∧ ( 𝐴 ∈ [ 𝑦 ] 𝑅 ∧ 𝐵 ∈ [ 𝑦 ] 𝑅 ) ) )
2 an32 ⊢ ( ( ( 𝑥 ∈ dom 𝑅 ∧ 𝑦 ∈ dom 𝑅 ) ∧ 𝐴 ∈ [ 𝑥 ] 𝑅 ) ↔ ( ( 𝑥 ∈ dom 𝑅 ∧ 𝐴 ∈ [ 𝑥 ] 𝑅 ) ∧ 𝑦 ∈ dom 𝑅 ) )
3 disjlem14 ⊢ ( Disj 𝑅 → ( ( 𝑥 ∈ dom 𝑅 ∧ 𝑦 ∈ dom 𝑅 ) → ( ( 𝐴 ∈ [ 𝑥 ] 𝑅 ∧ 𝐴 ∈ [ 𝑦 ] 𝑅 ) → [ 𝑥 ] 𝑅 = [ 𝑦 ] 𝑅 ) ) )
4 eleq2 ⊢ ( [ 𝑥 ] 𝑅 = [ 𝑦 ] 𝑅 → ( 𝐵 ∈ [ 𝑥 ] 𝑅 ↔ 𝐵 ∈ [ 𝑦 ] 𝑅 ) )
5 4 biimprd ⊢ ( [ 𝑥 ] 𝑅 = [ 𝑦 ] 𝑅 → ( 𝐵 ∈ [ 𝑦 ] 𝑅 → 𝐵 ∈ [ 𝑥 ] 𝑅 ) )
6 3 5 syl8 ⊢ ( Disj 𝑅 → ( ( 𝑥 ∈ dom 𝑅 ∧ 𝑦 ∈ dom 𝑅 ) → ( ( 𝐴 ∈ [ 𝑥 ] 𝑅 ∧ 𝐴 ∈ [ 𝑦 ] 𝑅 ) → ( 𝐵 ∈ [ 𝑦 ] 𝑅 → 𝐵 ∈ [ 𝑥 ] 𝑅 ) ) ) )
7 6 exp4a ⊢ ( Disj 𝑅 → ( ( 𝑥 ∈ dom 𝑅 ∧ 𝑦 ∈ dom 𝑅 ) → ( 𝐴 ∈ [ 𝑥 ] 𝑅 → ( 𝐴 ∈ [ 𝑦 ] 𝑅 → ( 𝐵 ∈ [ 𝑦 ] 𝑅 → 𝐵 ∈ [ 𝑥 ] 𝑅 ) ) ) ) )
8 7 impd ⊢ ( Disj 𝑅 → ( ( ( 𝑥 ∈ dom 𝑅 ∧ 𝑦 ∈ dom 𝑅 ) ∧ 𝐴 ∈ [ 𝑥 ] 𝑅 ) → ( 𝐴 ∈ [ 𝑦 ] 𝑅 → ( 𝐵 ∈ [ 𝑦 ] 𝑅 → 𝐵 ∈ [ 𝑥 ] 𝑅 ) ) ) )
9 2 8 biimtrrid ⊢ ( Disj 𝑅 → ( ( ( 𝑥 ∈ dom 𝑅 ∧ 𝐴 ∈ [ 𝑥 ] 𝑅 ) ∧ 𝑦 ∈ dom 𝑅 ) → ( 𝐴 ∈ [ 𝑦 ] 𝑅 → ( 𝐵 ∈ [ 𝑦 ] 𝑅 → 𝐵 ∈ [ 𝑥 ] 𝑅 ) ) ) )
10 9 expd ⊢ ( Disj 𝑅 → ( ( 𝑥 ∈ dom 𝑅 ∧ 𝐴 ∈ [ 𝑥 ] 𝑅 ) → ( 𝑦 ∈ dom 𝑅 → ( 𝐴 ∈ [ 𝑦 ] 𝑅 → ( 𝐵 ∈ [ 𝑦 ] 𝑅 → 𝐵 ∈ [ 𝑥 ] 𝑅 ) ) ) ) )
11 10 imp5a ⊢ ( Disj 𝑅 → ( ( 𝑥 ∈ dom 𝑅 ∧ 𝐴 ∈ [ 𝑥 ] 𝑅 ) → ( 𝑦 ∈ dom 𝑅 → ( ( 𝐴 ∈ [ 𝑦 ] 𝑅 ∧ 𝐵 ∈ [ 𝑦 ] 𝑅 ) → 𝐵 ∈ [ 𝑥 ] 𝑅 ) ) ) )
12 11 imp4b ⊢ ( ( Disj 𝑅 ∧ ( 𝑥 ∈ dom 𝑅 ∧ 𝐴 ∈ [ 𝑥 ] 𝑅 ) ) → ( ( 𝑦 ∈ dom 𝑅 ∧ ( 𝐴 ∈ [ 𝑦 ] 𝑅 ∧ 𝐵 ∈ [ 𝑦 ] 𝑅 ) ) → 𝐵 ∈ [ 𝑥 ] 𝑅 ) )
13 12 exlimdv ⊢ ( ( Disj 𝑅 ∧ ( 𝑥 ∈ dom 𝑅 ∧ 𝐴 ∈ [ 𝑥 ] 𝑅 ) ) → ( ∃ 𝑦 ( 𝑦 ∈ dom 𝑅 ∧ ( 𝐴 ∈ [ 𝑦 ] 𝑅 ∧ 𝐵 ∈ [ 𝑦 ] 𝑅 ) ) → 𝐵 ∈ [ 𝑥 ] 𝑅 ) )
14 1 13 biimtrid ⊢ ( ( Disj 𝑅 ∧ ( 𝑥 ∈ dom 𝑅 ∧ 𝐴 ∈ [ 𝑥 ] 𝑅 ) ) → ( ∃ 𝑦 ∈ dom 𝑅 ( 𝐴 ∈ [ 𝑦 ] 𝑅 ∧ 𝐵 ∈ [ 𝑦 ] 𝑅 ) → 𝐵 ∈ [ 𝑥 ] 𝑅 ) )
15 14 ex ⊢ ( Disj 𝑅 → ( ( 𝑥 ∈ dom 𝑅 ∧ 𝐴 ∈ [ 𝑥 ] 𝑅 ) → ( ∃ 𝑦 ∈ dom 𝑅 ( 𝐴 ∈ [ 𝑦 ] 𝑅 ∧ 𝐵 ∈ [ 𝑦 ] 𝑅 ) → 𝐵 ∈ [ 𝑥 ] 𝑅 ) ) )