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 ↾ 𝐴 ) ∧ 𝐵 ∈ 𝑢 ) → 𝑢 = [ 𝐵 ] ∼ 𝐴 ) ) )