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

Metamath Proof Explorer

Theorem disjlem18

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

Ref Expression
Assertion disjlem18 ⊢ A ∈ V ∧ B ∈ W → Disj R → x ∈ dom ⁡ R ∧ A ∈ x R → B ∈ x R ↔ A ≀ R B

Proof

Step Hyp Ref Expression
1 rspe ⊢ x ∈ dom ⁡ R ∧ A ∈ x R ∧ B ∈ x R → ∃ x ∈ dom ⁡ R A ∈ x R ∧ B ∈ x R
2 1 expr ⊢ x ∈ dom ⁡ R ∧ A ∈ x R → B ∈ x R → ∃ x ∈ dom ⁡ R A ∈ x R ∧ B ∈ x R
3 2 adantl ⊢ A ∈ V ∧ B ∈ W ∧ Disj R ∧ x ∈ dom ⁡ R ∧ A ∈ x R → B ∈ x R → ∃ x ∈ dom ⁡ R A ∈ x R ∧ B ∈ x R
4 relbrcoss ⊢ A ∈ V ∧ B ∈ W → Rel ⁡ R → A ≀ R B ↔ ∃ x ∈ dom ⁡ R A ∈ x R ∧ B ∈ x R
5 disjrel ⊢ Disj R → Rel ⁡ R
6 4 5 impel ⊢ A ∈ V ∧ B ∈ W ∧ Disj R → A ≀ R B ↔ ∃ x ∈ dom ⁡ R A ∈ x R ∧ B ∈ x R
7 6 adantr ⊢ A ∈ V ∧ B ∈ W ∧ Disj R ∧ x ∈ dom ⁡ R ∧ A ∈ x R → A ≀ R B ↔ ∃ x ∈ dom ⁡ R A ∈ x R ∧ B ∈ x R
8 3 7 sylibrd ⊢ A ∈ V ∧ B ∈ W ∧ Disj R ∧ x ∈ dom ⁡ R ∧ A ∈ x R → B ∈ x R → A ≀ R B
9 8 ex ⊢ A ∈ V ∧ B ∈ W ∧ Disj R → x ∈ dom ⁡ R ∧ A ∈ x R → B ∈ x R → A ≀ R B
10 disjlem17 ⊢ Disj R → x ∈ dom ⁡ R ∧ A ∈ x R → ∃ y ∈ dom ⁡ R A ∈ y R ∧ B ∈ y R → B ∈ x R
11 10 adantl ⊢ A ∈ V ∧ B ∈ W ∧ Disj R → x ∈ dom ⁡ R ∧ A ∈ x R → ∃ y ∈ dom ⁡ R A ∈ y R ∧ B ∈ y R → B ∈ x R
12 relbrcoss ⊢ A ∈ V ∧ B ∈ W → Rel ⁡ R → A ≀ R B ↔ ∃ y ∈ dom ⁡ R A ∈ y R ∧ B ∈ y R
13 12 5 impel ⊢ A ∈ V ∧ B ∈ W ∧ Disj R → A ≀ R B ↔ ∃ y ∈ dom ⁡ R A ∈ y R ∧ B ∈ y R
14 13 imbi1d ⊢ A ∈ V ∧ B ∈ W ∧ Disj R → A ≀ R B → B ∈ x R ↔ ∃ y ∈ dom ⁡ R A ∈ y R ∧ B ∈ y R → B ∈ x R
15 11 14 sylibrd ⊢ A ∈ V ∧ B ∈ W ∧ Disj R → x ∈ dom ⁡ R ∧ A ∈ x R → A ≀ R B → B ∈ x R
16 9 15 impbidd ⊢ A ∈ V ∧ B ∈ W ∧ Disj R → x ∈ dom ⁡ R ∧ A ∈ x R → B ∈ x R ↔ A ≀ R B
17 16 ex ⊢ A ∈ V ∧ B ∈ W → Disj R → x ∈ dom ⁡ R ∧ A ∈ x R → B ∈ x R ↔ A ≀ R B