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𝑉 )