disjdsct

Description: A disjoint collection is distinct, i.e. each set in this collection is different of all others, provided that it does not contain the empty set This can be expressed as "the converse of the mapping function is a function", or "the mapping function is single-rooted". (Cf. funcnv ) (Contributed by Thierry Arnoux, 28-Feb-2017)

	Ref	Expression
Hypotheses	disjdsct.0	⊢ Ⅎ 𝑥 𝜑
	disjdsct.1	⊢ Ⅎ 𝑥 𝐴
	disjdsct.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ( 𝑉 ∖ { ∅ } ) )
	disjdsct.3	⊢ ( 𝜑 → Disj 𝑥 ∈ 𝐴 𝐵 )
Assertion	disjdsct	⊢ ( 𝜑 → Fun ^◡ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		disjdsct.0	⊢ Ⅎ 𝑥 𝜑
2		disjdsct.1	⊢ Ⅎ 𝑥 𝐴
3		disjdsct.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ( 𝑉 ∖ { ∅ } ) )
4		disjdsct.3	⊢ ( 𝜑 → Disj 𝑥 ∈ 𝐴 𝐵 )
5	2	disjorsf	⊢ ( Disj 𝑥 ∈ 𝐴 𝐵 ↔ ∀ 𝑖 ∈ 𝐴 ∀ 𝑗 ∈ 𝐴 ( 𝑖 = 𝑗 ∨ ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ ) )
6	4 5	sylib	⊢ ( 𝜑 → ∀ 𝑖 ∈ 𝐴 ∀ 𝑗 ∈ 𝐴 ( 𝑖 = 𝑗 ∨ ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ ) )
7	6	r19.21bi	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ) → ∀ 𝑗 ∈ 𝐴 ( 𝑖 = 𝑗 ∨ ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ ) )
8	7	r19.21bi	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ) ∧ 𝑗 ∈ 𝐴 ) → ( 𝑖 = 𝑗 ∨ ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ ) )
9		simpr3	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐴 ∧ ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ ) ) → ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ )
10		eldifsni	⊢ ( 𝐵 ∈ ( 𝑉 ∖ { ∅ } ) → 𝐵 ≠ ∅ )
11	3 10	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ≠ ∅ )
12	11	sbimi	⊢ ( [ 𝑖 / 𝑥 ] ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → [ 𝑖 / 𝑥 ] 𝐵 ≠ ∅ )
13		sban	⊢ ( [ 𝑖 / 𝑥 ] ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ↔ ( [ 𝑖 / 𝑥 ] 𝜑 ∧ [ 𝑖 / 𝑥 ] 𝑥 ∈ 𝐴 ) )
14	1	sbf	⊢ ( [ 𝑖 / 𝑥 ] 𝜑 ↔ 𝜑 )
15	2	clelsb1fw	⊢ ( [ 𝑖 / 𝑥 ] 𝑥 ∈ 𝐴 ↔ 𝑖 ∈ 𝐴 )
16	14 15	anbi12i	⊢ ( ( [ 𝑖 / 𝑥 ] 𝜑 ∧ [ 𝑖 / 𝑥 ] 𝑥 ∈ 𝐴 ) ↔ ( 𝜑 ∧ 𝑖 ∈ 𝐴 ) )
17	13 16	bitri	⊢ ( [ 𝑖 / 𝑥 ] ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ↔ ( 𝜑 ∧ 𝑖 ∈ 𝐴 ) )
18		sbsbc	⊢ ( [ 𝑖 / 𝑥 ] 𝐵 ≠ ∅ ↔ [ 𝑖 / 𝑥 ] 𝐵 ≠ ∅ )
19		sbcne12	⊢ ( [ 𝑖 / 𝑥 ] 𝐵 ≠ ∅ ↔ ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ≠ ⦋ 𝑖 / 𝑥 ⦌ ∅ )
20		csb0	⊢ ⦋ 𝑖 / 𝑥 ⦌ ∅ = ∅
21	20	neeq2i	⊢ ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ≠ ⦋ 𝑖 / 𝑥 ⦌ ∅ ↔ ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ≠ ∅ )
22	18 19 21	3bitri	⊢ ( [ 𝑖 / 𝑥 ] 𝐵 ≠ ∅ ↔ ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ≠ ∅ )
23	12 17 22	3imtr3i	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ) → ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ≠ ∅ )
24	23	3ad2antr1	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐴 ∧ ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ ) ) → ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ≠ ∅ )
25		disj3	⊢ ( ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ ↔ ⦋ 𝑖 / 𝑥 ⦌ 𝐵 = ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∖ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) )
26	25	biimpi	⊢ ( ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ → ⦋ 𝑖 / 𝑥 ⦌ 𝐵 = ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∖ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) )
27	26	neeq1d	⊢ ( ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ → ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ≠ ∅ ↔ ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∖ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) ≠ ∅ ) )
28	27	biimpa	⊢ ( ( ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ ∧ ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ≠ ∅ ) → ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∖ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) ≠ ∅ )
29		difn0	⊢ ( ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∖ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) ≠ ∅ → ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ≠ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 )
30	28 29	syl	⊢ ( ( ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ ∧ ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ≠ ∅ ) → ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ≠ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 )
31	9 24 30	syl2anc	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐴 ∧ ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ ) ) → ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ≠ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 )
32	31	3anassrs	⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ) ∧ 𝑗 ∈ 𝐴 ) ∧ ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ ) → ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ≠ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 )
33	32	ex	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ) ∧ 𝑗 ∈ 𝐴 ) → ( ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ → ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ≠ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) )
34	33	orim2d	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ) ∧ 𝑗 ∈ 𝐴 ) → ( ( 𝑖 = 𝑗 ∨ ( ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) = ∅ ) → ( 𝑖 = 𝑗 ∨ ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ≠ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) ) )
35	8 34	mpd	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ) ∧ 𝑗 ∈ 𝐴 ) → ( 𝑖 = 𝑗 ∨ ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ≠ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) )
36	35	ralrimiva	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ) → ∀ 𝑗 ∈ 𝐴 ( 𝑖 = 𝑗 ∨ ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ≠ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) )
37	36	ralrimiva	⊢ ( 𝜑 → ∀ 𝑖 ∈ 𝐴 ∀ 𝑗 ∈ 𝐴 ( 𝑖 = 𝑗 ∨ ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ≠ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) )
38		nfmpt1	⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
39		eqid	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
40	1 2 38 39 3	funcnv4mpt	⊢ ( 𝜑 → ( Fun ^◡ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↔ ∀ 𝑖 ∈ 𝐴 ∀ 𝑗 ∈ 𝐴 ( 𝑖 = 𝑗 ∨ ⦋ 𝑖 / 𝑥 ⦌ 𝐵 ≠ ⦋ 𝑗 / 𝑥 ⦌ 𝐵 ) ) )
41	37 40	mpbird	⊢ ( 𝜑 → Fun ^◡ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )

Metamath Proof Explorer

Theorem disjdsct

Proof