Metamath Proof Explorer

Theorem eldisjlem19

Description: Special case of disjlem19 (together with membpartlem19 , this is former prtlem19 ). (Contributed by Peter Mazsa, 21-Oct-2021)

Ref Expression
Assertion eldisjlem19 ⊢ B ∈ V → ElDisj A → u ∈ dom ⁡ E -1 ↾ A ∧ B ∈ u → u = B ∼ A

Proof

Step Hyp Ref Expression
1 df-eldisj ⊢ ElDisj A ↔ Disj E -1 ↾ A
2 disjlem19 ⊢ B ∈ V → Disj E -1 ↾ A → u ∈ dom ⁡ E -1 ↾ A ∧ B ∈ u E -1 ↾ A → u E -1 ↾ A = B ≀ E -1 ↾ A
3 1 2 biimtrid ⊢ B ∈ V → ElDisj A → u ∈ dom ⁡ E -1 ↾ A ∧ B ∈ u E -1 ↾ A → u E -1 ↾ A = B ≀ E -1 ↾ A
4 3 imp ⊢ B ∈ V ∧ ElDisj A → u ∈ dom ⁡ E -1 ↾ A ∧ B ∈ u E -1 ↾ A → u E -1 ↾ A = B ≀ E -1 ↾ A
5 4 expdimp ⊢ B ∈ V ∧ ElDisj A ∧ u ∈ dom ⁡ E -1 ↾ A → B ∈ u E -1 ↾ A → u E -1 ↾ A = B ≀ E -1 ↾ A
6 eccnvepres3 ⊢ u ∈ dom ⁡ E -1 ↾ A → u E -1 ↾ A = u
7 6 eleq2d ⊢ u ∈ dom ⁡ E -1 ↾ A → B ∈ u E -1 ↾ A ↔ B ∈ u
8 6 eqeq1d ⊢ u ∈ dom ⁡ E -1 ↾ A → u E -1 ↾ A = B ≀ E -1 ↾ A ↔ u = B ≀ E -1 ↾ A
9 7 8 imbi12d ⊢ u ∈ dom ⁡ E -1 ↾ A → B ∈ u E -1 ↾ A → u E -1 ↾ A = B ≀ E -1 ↾ A ↔ B ∈ u → u = B ≀ E -1 ↾ A
10 9 adantl ⊢ B ∈ V ∧ ElDisj A ∧ u ∈ dom ⁡ E -1 ↾ A → B ∈ u E -1 ↾ A → u E -1 ↾ A = B ≀ E -1 ↾ A ↔ B ∈ u → u = B ≀ E -1 ↾ A
11 5 10 mpbid ⊢ B ∈ V ∧ ElDisj A ∧ u ∈ dom ⁡ E -1 ↾ A → B ∈ u → u = B ≀ E -1 ↾ A
12 df-coels ⊢ ∼ A = ≀ E -1 ↾ A
13 12 eceq2i ⊢ B ∼ A = B ≀ E -1 ↾ A
14 13 eqeq2i ⊢ u = B ∼ A ↔ u = B ≀ E -1 ↾ A
15 11 14 imbitrrdi ⊢ B ∈ V ∧ ElDisj A ∧ u ∈ dom ⁡ E -1 ↾ A → B ∈ u → u = B ∼ A
16 15 expimpd ⊢ B ∈ V ∧ ElDisj A → u ∈ dom ⁡ E -1 ↾ A ∧ B ∈ u → u = B ∼ A
17 16 ex ⊢ B ∈ V → ElDisj A → u ∈ dom ⁡ E -1 ↾ A ∧ B ∈ u → u = B ∼ A