Metamath Proof Explorer

Theorem disjf1

Description: A 1 to 1 mapping built from disjoint, nonempty sets. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses disjf1.xph ⊢ Ⅎ 𝑥 𝜑
disjf1.f ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
disjf1.b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
disjf1.n0 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ≠ ∅ )
disjf1.dj ⊢ ( 𝜑 → Disj 𝑥 ∈ 𝐴 𝐵 )
Assertion disjf1 ( 𝜑 → 𝐹 : 𝐴 –1-1→ 𝑉 )

Proof

Step Hyp Ref Expression
1 disjf1.xph ⊢ Ⅎ 𝑥 𝜑
2 disjf1.f ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
3 disjf1.b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
4 disjf1.n0 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ≠ ∅ )
5 disjf1.dj ⊢ ( 𝜑 → Disj 𝑥 ∈ 𝐴 𝐵 )
6 nfv ⊢ Ⅎ 𝑥 𝑦 ∈ 𝐴
7 1 6 nfan ⊢ Ⅎ 𝑥 ( 𝜑 ∧ 𝑦 ∈ 𝐴 )
8 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐵
9 nfcv ⊢ Ⅎ 𝑥 𝑉
10 8 9 nfel ⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∈ 𝑉
11 7 10 nfim ⊢ Ⅎ 𝑥 ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∈ 𝑉 )
12 eleq1w ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴 ) )
13 12 anbi2d ⊢ ( 𝑥 = 𝑦 → ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ↔ ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) ) )
14 csbeq1a ⊢ ( 𝑥 = 𝑦 → 𝐵 = ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
15 14 eleq1d ⊢ ( 𝑥 = 𝑦 → ( 𝐵 ∈ 𝑉 ↔ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∈ 𝑉 ) )
16 13 15 imbi12d ⊢ ( 𝑥 = 𝑦 → ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 ) ↔ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∈ 𝑉 ) ) )
17 11 16 3 chvarfv ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∈ 𝑉 )
18 17 ralrimiva ⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝐴 ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∈ 𝑉 )
19 inidm ⊢ ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) = ⦋ 𝑦 / 𝑥 ⦌ 𝐵
20 19 eqcomi ⊢ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 = ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
21 20 a1i ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) ∧ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 = ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ∧ ¬ 𝑦 = 𝑧 ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 = ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) )
22 ineq2 ⊢ ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 = ⦋ 𝑧 / 𝑥 ⦌ 𝐵 → ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) = ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) )
23 22 ad2antlr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) ∧ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 = ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ∧ ¬ 𝑦 = 𝑧 ) → ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) = ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) )
24 nfcv ⊢ Ⅎ 𝑤 𝐵
25 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑤 / 𝑥 ⦌ 𝐵
26 csbeq1a ⊢ ( 𝑥 = 𝑤 → 𝐵 = ⦋ 𝑤 / 𝑥 ⦌ 𝐵 )
27 24 25 26 cbvdisj ⊢ ( Disj 𝑥 ∈ 𝐴 𝐵 ↔ Disj 𝑤 ∈ 𝐴 ⦋ 𝑤 / 𝑥 ⦌ 𝐵 )
28 5 27 sylib ⊢ ( 𝜑 → Disj 𝑤 ∈ 𝐴 ⦋ 𝑤 / 𝑥 ⦌ 𝐵 )
29 28 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) ∧ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 = ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ∧ ¬ 𝑦 = 𝑧 ) → Disj 𝑤 ∈ 𝐴 ⦋ 𝑤 / 𝑥 ⦌ 𝐵 )
30 simpllr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) ∧ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 = ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ∧ ¬ 𝑦 = 𝑧 ) → ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) )
31 neqne ⊢ ( ¬ 𝑦 = 𝑧 → 𝑦 ≠ 𝑧 )
32 31 adantl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) ∧ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 = ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ∧ ¬ 𝑦 = 𝑧 ) → 𝑦 ≠ 𝑧 )
33 csbeq1 ⊢ ( 𝑤 = 𝑦 → ⦋ 𝑤 / 𝑥 ⦌ 𝐵 = ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
34 csbeq1 ⊢ ( 𝑤 = 𝑧 → ⦋ 𝑤 / 𝑥 ⦌ 𝐵 = ⦋ 𝑧 / 𝑥 ⦌ 𝐵 )
35 33 34 disji2 ⊢ ( ( Disj 𝑤 ∈ 𝐴 ⦋ 𝑤 / 𝑥 ⦌ 𝐵 ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑦 ≠ 𝑧 ) → ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) = ∅ )
36 29 30 32 35 syl3anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) ∧ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 = ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ∧ ¬ 𝑦 = 𝑧 ) → ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∩ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) = ∅ )
37 21 23 36 3eqtrd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) ∧ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 = ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ∧ ¬ 𝑦 = 𝑧 ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 = ∅ )
38 nfcv ⊢ Ⅎ 𝑥 ∅
39 8 38 nfne ⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ≠ ∅
40 7 39 nfim ⊢ Ⅎ 𝑥 ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ≠ ∅ )
41 14 neeq1d ⊢ ( 𝑥 = 𝑦 → ( 𝐵 ≠ ∅ ↔ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ≠ ∅ ) )
42 13 41 imbi12d ⊢ ( 𝑥 = 𝑦 → ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ≠ ∅ ) ↔ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ≠ ∅ ) ) )
43 40 42 4 chvarfv ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ≠ ∅ )
44 43 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ≠ ∅ )
45 44 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) ∧ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 = ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ∧ ¬ 𝑦 = 𝑧 ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ≠ ∅ )
46 45 neneqd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) ∧ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 = ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ∧ ¬ 𝑦 = 𝑧 ) → ¬ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 = ∅ )
47 37 46 condan ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) ∧ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 = ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) → 𝑦 = 𝑧 )
48 47 ex ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) → ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 = ⦋ 𝑧 / 𝑥 ⦌ 𝐵 → 𝑦 = 𝑧 ) )
49 48 ralrimivva ⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 = ⦋ 𝑧 / 𝑥 ⦌ 𝐵 → 𝑦 = 𝑧 ) )
50 18 49 jca ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ 𝐴 ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 = ⦋ 𝑧 / 𝑥 ⦌ 𝐵 → 𝑦 = 𝑧 ) ) )
51 nfcv ⊢ Ⅎ 𝑦 𝐵
52 51 8 14 cbvmpt ⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑦 ∈ 𝐴 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
53 2 52 eqtri ⊢ 𝐹 = ( 𝑦 ∈ 𝐴 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
54 csbeq1 ⊢ ( 𝑦 = 𝑧 → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 = ⦋ 𝑧 / 𝑥 ⦌ 𝐵 )
55 53 54 f1mpt ⊢ ( 𝐹 : 𝐴 –1-1→ 𝑉 ↔ ( ∀ 𝑦 ∈ 𝐴 ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∈ 𝑉 ∧ ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ 𝐴 ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 = ⦋ 𝑧 / 𝑥 ⦌ 𝐵 → 𝑦 = 𝑧 ) ) )
56 50 55 sylibr ⊢ ( 𝜑 → 𝐹 : 𝐴 –1-1→ 𝑉 )