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 𝑥 ∈ 𝐴 𝐵 )