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 R → x ∈ dom ⁡ R ∧ A ∈ x R → ∃ y ∈ dom ⁡ R A ∈ y R ∧ B ∈ y R → B ∈ x R

Proof

Step Hyp Ref Expression
1 df-rex ⊢ ∃ y ∈ dom ⁡ R A ∈ y R ∧ B ∈ y R ↔ ∃ y y ∈ dom ⁡ R ∧ A ∈ y R ∧ B ∈ y R
2 an32 ⊢ x ∈ dom ⁡ R ∧ y ∈ dom ⁡ R ∧ A ∈ x R ↔ x ∈ dom ⁡ R ∧ A ∈ x R ∧ y ∈ dom ⁡ R
3 disjlem14 ⊢ Disj R → x ∈ dom ⁡ R ∧ y ∈ dom ⁡ R → A ∈ x R ∧ A ∈ y R → x R = y R
4 eleq2 ⊢ x R = y R → B ∈ x R ↔ B ∈ y R
5 4 biimprd ⊢ x R = y R → B ∈ y R → B ∈ x R
6 3 5 syl8 ⊢ Disj R → x ∈ dom ⁡ R ∧ y ∈ dom ⁡ R → A ∈ x R ∧ A ∈ y R → B ∈ y R → B ∈ x R
7 6 exp4a ⊢ Disj R → x ∈ dom ⁡ R ∧ y ∈ dom ⁡ R → A ∈ x R → A ∈ y R → B ∈ y R → B ∈ x R
8 7 impd ⊢ Disj R → x ∈ dom ⁡ R ∧ y ∈ dom ⁡ R ∧ A ∈ x R → A ∈ y R → B ∈ y R → B ∈ x R
9 2 8 biimtrrid ⊢ Disj R → x ∈ dom ⁡ R ∧ A ∈ x R ∧ y ∈ dom ⁡ R → A ∈ y R → B ∈ y R → B ∈ x R
10 9 expd ⊢ Disj R → x ∈ dom ⁡ R ∧ A ∈ x R → y ∈ dom ⁡ R → A ∈ y R → B ∈ y R → B ∈ x R
11 10 imp5a ⊢ Disj R → x ∈ dom ⁡ R ∧ A ∈ x R → y ∈ dom ⁡ R → A ∈ y R ∧ B ∈ y R → B ∈ x R
12 11 imp4b ⊢ Disj R ∧ x ∈ dom ⁡ R ∧ A ∈ x R → y ∈ dom ⁡ R ∧ A ∈ y R ∧ B ∈ y R → B ∈ x R
13 12 exlimdv ⊢ Disj R ∧ x ∈ dom ⁡ R ∧ A ∈ x R → ∃ y y ∈ dom ⁡ R ∧ A ∈ y R ∧ B ∈ y R → B ∈ x R
14 1 13 biimtrid ⊢ Disj R ∧ x ∈ dom ⁡ R ∧ A ∈ x R → ∃ y ∈ dom ⁡ R A ∈ y R ∧ B ∈ y R → B ∈ x R
15 14 ex ⊢ Disj R → x ∈ dom ⁡ R ∧ A ∈ x R → ∃ y ∈ dom ⁡ R A ∈ y R ∧ B ∈ y R → B ∈ x R