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

Metamath Proof Explorer

Theorem invdisj

Description: If there is a function C ( y ) such that C ( y ) = x for all y e. B ( x ) , then the sets B ( x ) for distinct x e. A are disjoint. (Contributed by Mario Carneiro, 10-Dec-2016)

Ref Expression
Assertion invdisj ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝐶 = 𝑥 → Disj 𝑥 ∈ 𝐴 𝐵 )

Proof

Step Hyp Ref Expression
1 nfra2w ⊢ Ⅎ 𝑦 ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝐶 = 𝑥
2 df-ral ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝐶 = 𝑥 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ∀ 𝑦 ∈ 𝐵 𝐶 = 𝑥 ) )
3 rsp ⊢ ( ∀ 𝑦 ∈ 𝐵 𝐶 = 𝑥 → ( 𝑦 ∈ 𝐵 → 𝐶 = 𝑥 ) )
4 eqcom ⊢ ( 𝐶 = 𝑥 ↔ 𝑥 = 𝐶 )
5 3 4 imbitrdi ⊢ ( ∀ 𝑦 ∈ 𝐵 𝐶 = 𝑥 → ( 𝑦 ∈ 𝐵 → 𝑥 = 𝐶 ) )
6 5 imim2i ⊢ ( ( 𝑥 ∈ 𝐴 → ∀ 𝑦 ∈ 𝐵 𝐶 = 𝑥 ) → ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐵 → 𝑥 = 𝐶 ) ) )
7 6 impd ⊢ ( ( 𝑥 ∈ 𝐴 → ∀ 𝑦 ∈ 𝐵 𝐶 = 𝑥 ) → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → 𝑥 = 𝐶 ) )
8 7 alimi ⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → ∀ 𝑦 ∈ 𝐵 𝐶 = 𝑥 ) → ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → 𝑥 = 𝐶 ) )
9 2 8 sylbi ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝐶 = 𝑥 → ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → 𝑥 = 𝐶 ) )
10 mo2icl ⊢ ( ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → 𝑥 = 𝐶 ) → ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) )
11 9 10 syl ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝐶 = 𝑥 → ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) )
12 1 11 alrimi ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝐶 = 𝑥 → ∀ 𝑦 ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) )
13 dfdisj2 ⊢ ( Disj 𝑥 ∈ 𝐴 𝐵 ↔ ∀ 𝑦 ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) )
14 12 13 sylibr ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝐶 = 𝑥 → Disj 𝑥 ∈ 𝐴 𝐵 )