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

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 ( 𝐵 ∈ 𝑉 → ( ElDisj 𝐴 → ( ( 𝑢 ∈ dom ( ◡ E ↾ 𝐴 ) ∧ 𝐵 ∈ 𝑢 ) → 𝑢 = [ 𝐵 ] ∼ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 df-eldisj ⊢ ( ElDisj 𝐴 ↔ Disj ( ◡ E ↾ 𝐴 ) )
2 disjlem19 ⊢ ( 𝐵 ∈ 𝑉 → ( Disj ( ◡ E ↾ 𝐴 ) → ( ( 𝑢 ∈ dom ( ◡ E ↾ 𝐴 ) ∧ 𝐵 ∈ [ 𝑢 ] ( ◡ E ↾ 𝐴 ) ) → [ 𝑢 ] ( ◡ E ↾ 𝐴 ) = [ 𝐵 ] ≀ ( ◡ E ↾ 𝐴 ) ) ) )
3 1 2 biimtrid ⊢ ( 𝐵 ∈ 𝑉 → ( ElDisj 𝐴 → ( ( 𝑢 ∈ dom ( ◡ E ↾ 𝐴 ) ∧ 𝐵 ∈ [ 𝑢 ] ( ◡ E ↾ 𝐴 ) ) → [ 𝑢 ] ( ◡ E ↾ 𝐴 ) = [ 𝐵 ] ≀ ( ◡ E ↾ 𝐴 ) ) ) )
4 3 imp ⊢ ( ( 𝐵 ∈ 𝑉 ∧ ElDisj 𝐴 ) → ( ( 𝑢 ∈ dom ( ◡ E ↾ 𝐴 ) ∧ 𝐵 ∈ [ 𝑢 ] ( ◡ E ↾ 𝐴 ) ) → [ 𝑢 ] ( ◡ E ↾ 𝐴 ) = [ 𝐵 ] ≀ ( ◡ E ↾ 𝐴 ) ) )
5 4 expdimp ⊢ ( ( ( 𝐵 ∈ 𝑉 ∧ ElDisj 𝐴 ) ∧ 𝑢 ∈ dom ( ◡ E ↾ 𝐴 ) ) → ( 𝐵 ∈ [ 𝑢 ] ( ◡ E ↾ 𝐴 ) → [ 𝑢 ] ( ◡ E ↾ 𝐴 ) = [ 𝐵 ] ≀ ( ◡ E ↾ 𝐴 ) ) )
6 eccnvepres3 ⊢ ( 𝑢 ∈ dom ( ◡ E ↾ 𝐴 ) → [ 𝑢 ] ( ◡ E ↾ 𝐴 ) = 𝑢 )
7 6 eleq2d ⊢ ( 𝑢 ∈ dom ( ◡ E ↾ 𝐴 ) → ( 𝐵 ∈ [ 𝑢 ] ( ◡ E ↾ 𝐴 ) ↔ 𝐵 ∈ 𝑢 ) )
8 6 eqeq1d ⊢ ( 𝑢 ∈ dom ( ◡ E ↾ 𝐴 ) → ( [ 𝑢 ] ( ◡ E ↾ 𝐴 ) = [ 𝐵 ] ≀ ( ◡ E ↾ 𝐴 ) ↔ 𝑢 = [ 𝐵 ] ≀ ( ◡ E ↾ 𝐴 ) ) )
9 7 8 imbi12d ⊢ ( 𝑢 ∈ dom ( ◡ E ↾ 𝐴 ) → ( ( 𝐵 ∈ [ 𝑢 ] ( ◡ E ↾ 𝐴 ) → [ 𝑢 ] ( ◡ E ↾ 𝐴 ) = [ 𝐵 ] ≀ ( ◡ E ↾ 𝐴 ) ) ↔ ( 𝐵 ∈ 𝑢 → 𝑢 = [ 𝐵 ] ≀ ( ◡ E ↾ 𝐴 ) ) ) )
10 9 adantl ⊢ ( ( ( 𝐵 ∈ 𝑉 ∧ ElDisj 𝐴 ) ∧ 𝑢 ∈ dom ( ◡ E ↾ 𝐴 ) ) → ( ( 𝐵 ∈ [ 𝑢 ] ( ◡ E ↾ 𝐴 ) → [ 𝑢 ] ( ◡ E ↾ 𝐴 ) = [ 𝐵 ] ≀ ( ◡ E ↾ 𝐴 ) ) ↔ ( 𝐵 ∈ 𝑢 → 𝑢 = [ 𝐵 ] ≀ ( ◡ E ↾ 𝐴 ) ) ) )
11 5 10 mpbid ⊢ ( ( ( 𝐵 ∈ 𝑉 ∧ ElDisj 𝐴 ) ∧ 𝑢 ∈ dom ( ◡ E ↾ 𝐴 ) ) → ( 𝐵 ∈ 𝑢 → 𝑢 = [ 𝐵 ] ≀ ( ◡ E ↾ 𝐴 ) ) )
12 df-coels ⊢ ∼ 𝐴 = ≀ ( ◡ E ↾ 𝐴 )
13 12 eceq2i ⊢ [ 𝐵 ] ∼ 𝐴 = [ 𝐵 ] ≀ ( ◡ E ↾ 𝐴 )
14 13 eqeq2i ⊢ ( 𝑢 = [ 𝐵 ] ∼ 𝐴 ↔ 𝑢 = [ 𝐵 ] ≀ ( ◡ E ↾ 𝐴 ) )
15 11 14 imbitrrdi ⊢ ( ( ( 𝐵 ∈ 𝑉 ∧ ElDisj 𝐴 ) ∧ 𝑢 ∈ dom ( ◡ E ↾ 𝐴 ) ) → ( 𝐵 ∈ 𝑢 → 𝑢 = [ 𝐵 ] ∼ 𝐴 ) )
16 15 expimpd ⊢ ( ( 𝐵 ∈ 𝑉 ∧ ElDisj 𝐴 ) → ( ( 𝑢 ∈ dom ( ◡ E ↾ 𝐴 ) ∧ 𝐵 ∈ 𝑢 ) → 𝑢 = [ 𝐵 ] ∼ 𝐴 ) )
17 16 ex ⊢ ( 𝐵 ∈ 𝑉 → ( ElDisj 𝐴 → ( ( 𝑢 ∈ dom ( ◡ E ↾ 𝐴 ) ∧ 𝐵 ∈ 𝑢 ) → 𝑢 = [ 𝐵 ] ∼ 𝐴 ) ) )