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

Metamath Proof Explorer

Theorem membpartlem19

Description: Together with disjlem19 , this is former prtlem19 . (Contributed by Rodolfo Medina, 15-Oct-2010) (Revised by Mario Carneiro, 12-Aug-2015) (Revised by Peter Mazsa, 21-Oct-2021)

Ref Expression
Assertion membpartlem19 ( 𝐵 ∈ 𝑉 → ( MembPart 𝐴 → ( ( 𝑢 ∈ 𝐴 ∧ 𝐵 ∈ 𝑢 ) → 𝑢 = [ 𝐵 ] ∼ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 dfmembpart2 ⊢ ( MembPart 𝐴 ↔ ( ElDisj 𝐴 ∧ ¬ ∅ ∈ 𝐴 ) )
2 n0el2 ⊢ ( ¬ ∅ ∈ 𝐴 ↔ dom ( ◡ E ↾ 𝐴 ) = 𝐴 )
3 2 biimpi ⊢ ( ¬ ∅ ∈ 𝐴 → dom ( ◡ E ↾ 𝐴 ) = 𝐴 )
4 3 ad2antll ⊢ ( ( 𝐵 ∈ 𝑉 ∧ ( ElDisj 𝐴 ∧ ¬ ∅ ∈ 𝐴 ) ) → dom ( ◡ E ↾ 𝐴 ) = 𝐴 )
5 4 eleq2d ⊢ ( ( 𝐵 ∈ 𝑉 ∧ ( ElDisj 𝐴 ∧ ¬ ∅ ∈ 𝐴 ) ) → ( 𝑢 ∈ dom ( ◡ E ↾ 𝐴 ) ↔ 𝑢 ∈ 𝐴 ) )
6 eldisjlem19 ⊢ ( 𝐵 ∈ 𝑉 → ( ElDisj 𝐴 → ( ( 𝑢 ∈ dom ( ◡ E ↾ 𝐴 ) ∧ 𝐵 ∈ 𝑢 ) → 𝑢 = [ 𝐵 ] ∼ 𝐴 ) ) )
7 6 adantrd ⊢ ( 𝐵 ∈ 𝑉 → ( ( ElDisj 𝐴 ∧ ¬ ∅ ∈ 𝐴 ) → ( ( 𝑢 ∈ dom ( ◡ E ↾ 𝐴 ) ∧ 𝐵 ∈ 𝑢 ) → 𝑢 = [ 𝐵 ] ∼ 𝐴 ) ) )
8 7 imp ⊢ ( ( 𝐵 ∈ 𝑉 ∧ ( ElDisj 𝐴 ∧ ¬ ∅ ∈ 𝐴 ) ) → ( ( 𝑢 ∈ dom ( ◡ E ↾ 𝐴 ) ∧ 𝐵 ∈ 𝑢 ) → 𝑢 = [ 𝐵 ] ∼ 𝐴 ) )
9 8 expd ⊢ ( ( 𝐵 ∈ 𝑉 ∧ ( ElDisj 𝐴 ∧ ¬ ∅ ∈ 𝐴 ) ) → ( 𝑢 ∈ dom ( ◡ E ↾ 𝐴 ) → ( 𝐵 ∈ 𝑢 → 𝑢 = [ 𝐵 ] ∼ 𝐴 ) ) )
10 5 9 sylbird ⊢ ( ( 𝐵 ∈ 𝑉 ∧ ( ElDisj 𝐴 ∧ ¬ ∅ ∈ 𝐴 ) ) → ( 𝑢 ∈ 𝐴 → ( 𝐵 ∈ 𝑢 → 𝑢 = [ 𝐵 ] ∼ 𝐴 ) ) )
11 1 10 sylan2b ⊢ ( ( 𝐵 ∈ 𝑉 ∧ MembPart 𝐴 ) → ( 𝑢 ∈ 𝐴 → ( 𝐵 ∈ 𝑢 → 𝑢 = [ 𝐵 ] ∼ 𝐴 ) ) )
12 11 impd ⊢ ( ( 𝐵 ∈ 𝑉 ∧ MembPart 𝐴 ) → ( ( 𝑢 ∈ 𝐴 ∧ 𝐵 ∈ 𝑢 ) → 𝑢 = [ 𝐵 ] ∼ 𝐴 ) )
13 12 ex ⊢ ( 𝐵 ∈ 𝑉 → ( MembPart 𝐴 → ( ( 𝑢 ∈ 𝐴 ∧ 𝐵 ∈ 𝑢 ) → 𝑢 = [ 𝐵 ] ∼ 𝐴 ) ) )