Proof of Theorem f1oun2prg
Step | Hyp | Ref
| Expression |
1 | | simpl 483 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐴 ∈ 𝑉) |
2 | | 0z 12330 |
. . . . . . 7
⊢ 0 ∈
ℤ |
3 | 1, 2 | jctil 520 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (0 ∈ ℤ ∧ 𝐴 ∈ 𝑉)) |
4 | 3 | ad2antrr 723 |
. . . . 5
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌)) ∧ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷))) → (0 ∈ ℤ ∧ 𝐴 ∈ 𝑉)) |
5 | | simpr 485 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝐵 ∈ 𝑊) |
6 | | 1z 12350 |
. . . . . . 7
⊢ 1 ∈
ℤ |
7 | 5, 6 | jctil 520 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (1 ∈ ℤ ∧ 𝐵 ∈ 𝑊)) |
8 | 7 | ad2antrr 723 |
. . . . 5
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌)) ∧ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷))) → (1 ∈ ℤ ∧ 𝐵 ∈ 𝑊)) |
9 | 4, 8 | jca 512 |
. . . 4
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌)) ∧ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷))) → ((0 ∈ ℤ ∧ 𝐴 ∈ 𝑉) ∧ (1 ∈ ℤ ∧ 𝐵 ∈ 𝑊))) |
10 | | id 22 |
. . . . . . . 8
⊢ (𝐴 ≠ 𝐵 → 𝐴 ≠ 𝐵) |
11 | 10 | 3ad2ant1 1132 |
. . . . . . 7
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) → 𝐴 ≠ 𝐵) |
12 | | 0ne1 12044 |
. . . . . . 7
⊢ 0 ≠
1 |
13 | 11, 12 | jctil 520 |
. . . . . 6
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) → (0 ≠ 1 ∧ 𝐴 ≠ 𝐵)) |
14 | 13 | adantr 481 |
. . . . 5
⊢ (((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷)) → (0 ≠ 1 ∧ 𝐴 ≠ 𝐵)) |
15 | 14 | adantl 482 |
. . . 4
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌)) ∧ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷))) → (0 ≠ 1 ∧ 𝐴 ≠ 𝐵)) |
16 | | f1oprg 6758 |
. . . 4
⊢ (((0
∈ ℤ ∧ 𝐴
∈ 𝑉) ∧ (1 ∈
ℤ ∧ 𝐵 ∈
𝑊)) → ((0 ≠ 1 ∧
𝐴 ≠ 𝐵) → {〈0, 𝐴〉, 〈1, 𝐵〉}:{0, 1}–1-1-onto→{𝐴, 𝐵})) |
17 | 9, 15, 16 | sylc 65 |
. . 3
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌)) ∧ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷))) → {〈0, 𝐴〉, 〈1, 𝐵〉}:{0, 1}–1-1-onto→{𝐴, 𝐵}) |
18 | | simpl 483 |
. . . . . . . 8
⊢ ((𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌) → 𝐶 ∈ 𝑋) |
19 | | 2nn 12046 |
. . . . . . . 8
⊢ 2 ∈
ℕ |
20 | 18, 19 | jctil 520 |
. . . . . . 7
⊢ ((𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌) → (2 ∈ ℕ ∧ 𝐶 ∈ 𝑋)) |
21 | 20 | adantl 482 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌)) → (2 ∈ ℕ ∧ 𝐶 ∈ 𝑋)) |
22 | | simpr 485 |
. . . . . . . 8
⊢ ((𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌) → 𝐷 ∈ 𝑌) |
23 | | 3nn 12052 |
. . . . . . . 8
⊢ 3 ∈
ℕ |
24 | 22, 23 | jctil 520 |
. . . . . . 7
⊢ ((𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌) → (3 ∈ ℕ ∧ 𝐷 ∈ 𝑌)) |
25 | 24 | adantl 482 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌)) → (3 ∈ ℕ ∧ 𝐷 ∈ 𝑌)) |
26 | 21, 25 | jca 512 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌)) → ((2 ∈ ℕ ∧ 𝐶 ∈ 𝑋) ∧ (3 ∈ ℕ ∧ 𝐷 ∈ 𝑌))) |
27 | 26 | adantr 481 |
. . . 4
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌)) ∧ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷))) → ((2 ∈ ℕ ∧ 𝐶 ∈ 𝑋) ∧ (3 ∈ ℕ ∧ 𝐷 ∈ 𝑌))) |
28 | | id 22 |
. . . . . . . 8
⊢ (𝐶 ≠ 𝐷 → 𝐶 ≠ 𝐷) |
29 | 28 | 3ad2ant3 1134 |
. . . . . . 7
⊢ ((𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷) → 𝐶 ≠ 𝐷) |
30 | | 2re 12047 |
. . . . . . . 8
⊢ 2 ∈
ℝ |
31 | | 2lt3 12145 |
. . . . . . . 8
⊢ 2 <
3 |
32 | 30, 31 | ltneii 11088 |
. . . . . . 7
⊢ 2 ≠
3 |
33 | 29, 32 | jctil 520 |
. . . . . 6
⊢ ((𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷) → (2 ≠ 3 ∧ 𝐶 ≠ 𝐷)) |
34 | 33 | adantl 482 |
. . . . 5
⊢ (((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷)) → (2 ≠ 3 ∧ 𝐶 ≠ 𝐷)) |
35 | 34 | adantl 482 |
. . . 4
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌)) ∧ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷))) → (2 ≠ 3 ∧ 𝐶 ≠ 𝐷)) |
36 | | f1oprg 6758 |
. . . 4
⊢ (((2
∈ ℕ ∧ 𝐶
∈ 𝑋) ∧ (3 ∈
ℕ ∧ 𝐷 ∈
𝑌)) → ((2 ≠ 3 ∧
𝐶 ≠ 𝐷) → {〈2, 𝐶〉, 〈3, 𝐷〉}:{2, 3}–1-1-onto→{𝐶, 𝐷})) |
37 | 27, 35, 36 | sylc 65 |
. . 3
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌)) ∧ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷))) → {〈2, 𝐶〉, 〈3, 𝐷〉}:{2, 3}–1-1-onto→{𝐶, 𝐷}) |
38 | | disjsn2 4654 |
. . . . . . . . . 10
⊢ (𝐴 ≠ 𝐶 → ({𝐴} ∩ {𝐶}) = ∅) |
39 | 38 | 3ad2ant2 1133 |
. . . . . . . . 9
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) → ({𝐴} ∩ {𝐶}) = ∅) |
40 | | disjsn2 4654 |
. . . . . . . . . 10
⊢ (𝐵 ≠ 𝐶 → ({𝐵} ∩ {𝐶}) = ∅) |
41 | 40 | 3ad2ant1 1132 |
. . . . . . . . 9
⊢ ((𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷) → ({𝐵} ∩ {𝐶}) = ∅) |
42 | 39, 41 | anim12i 613 |
. . . . . . . 8
⊢ (((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷)) → (({𝐴} ∩ {𝐶}) = ∅ ∧ ({𝐵} ∩ {𝐶}) = ∅)) |
43 | 42 | adantl 482 |
. . . . . . 7
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌)) ∧ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷))) → (({𝐴} ∩ {𝐶}) = ∅ ∧ ({𝐵} ∩ {𝐶}) = ∅)) |
44 | | df-pr 4570 |
. . . . . . . . . 10
⊢ {𝐴, 𝐵} = ({𝐴} ∪ {𝐵}) |
45 | 44 | ineq1i 4148 |
. . . . . . . . 9
⊢ ({𝐴, 𝐵} ∩ {𝐶}) = (({𝐴} ∪ {𝐵}) ∩ {𝐶}) |
46 | 45 | eqeq1i 2745 |
. . . . . . . 8
⊢ (({𝐴, 𝐵} ∩ {𝐶}) = ∅ ↔ (({𝐴} ∪ {𝐵}) ∩ {𝐶}) = ∅) |
47 | | undisj1 4401 |
. . . . . . . 8
⊢ ((({𝐴} ∩ {𝐶}) = ∅ ∧ ({𝐵} ∩ {𝐶}) = ∅) ↔ (({𝐴} ∪ {𝐵}) ∩ {𝐶}) = ∅) |
48 | 46, 47 | bitr4i 277 |
. . . . . . 7
⊢ (({𝐴, 𝐵} ∩ {𝐶}) = ∅ ↔ (({𝐴} ∩ {𝐶}) = ∅ ∧ ({𝐵} ∩ {𝐶}) = ∅)) |
49 | 43, 48 | sylibr 233 |
. . . . . 6
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌)) ∧ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷))) → ({𝐴, 𝐵} ∩ {𝐶}) = ∅) |
50 | | disjsn2 4654 |
. . . . . . . . . 10
⊢ (𝐴 ≠ 𝐷 → ({𝐴} ∩ {𝐷}) = ∅) |
51 | 50 | 3ad2ant3 1134 |
. . . . . . . . 9
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) → ({𝐴} ∩ {𝐷}) = ∅) |
52 | | disjsn2 4654 |
. . . . . . . . . 10
⊢ (𝐵 ≠ 𝐷 → ({𝐵} ∩ {𝐷}) = ∅) |
53 | 52 | 3ad2ant2 1133 |
. . . . . . . . 9
⊢ ((𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷) → ({𝐵} ∩ {𝐷}) = ∅) |
54 | 51, 53 | anim12i 613 |
. . . . . . . 8
⊢ (((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷)) → (({𝐴} ∩ {𝐷}) = ∅ ∧ ({𝐵} ∩ {𝐷}) = ∅)) |
55 | 54 | adantl 482 |
. . . . . . 7
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌)) ∧ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷))) → (({𝐴} ∩ {𝐷}) = ∅ ∧ ({𝐵} ∩ {𝐷}) = ∅)) |
56 | 44 | ineq1i 4148 |
. . . . . . . . 9
⊢ ({𝐴, 𝐵} ∩ {𝐷}) = (({𝐴} ∪ {𝐵}) ∩ {𝐷}) |
57 | 56 | eqeq1i 2745 |
. . . . . . . 8
⊢ (({𝐴, 𝐵} ∩ {𝐷}) = ∅ ↔ (({𝐴} ∪ {𝐵}) ∩ {𝐷}) = ∅) |
58 | | undisj1 4401 |
. . . . . . . 8
⊢ ((({𝐴} ∩ {𝐷}) = ∅ ∧ ({𝐵} ∩ {𝐷}) = ∅) ↔ (({𝐴} ∪ {𝐵}) ∩ {𝐷}) = ∅) |
59 | 57, 58 | bitr4i 277 |
. . . . . . 7
⊢ (({𝐴, 𝐵} ∩ {𝐷}) = ∅ ↔ (({𝐴} ∩ {𝐷}) = ∅ ∧ ({𝐵} ∩ {𝐷}) = ∅)) |
60 | 55, 59 | sylibr 233 |
. . . . . 6
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌)) ∧ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷))) → ({𝐴, 𝐵} ∩ {𝐷}) = ∅) |
61 | 49, 60 | jca 512 |
. . . . 5
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌)) ∧ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷))) → (({𝐴, 𝐵} ∩ {𝐶}) = ∅ ∧ ({𝐴, 𝐵} ∩ {𝐷}) = ∅)) |
62 | | undisj2 4402 |
. . . . . 6
⊢ ((({𝐴, 𝐵} ∩ {𝐶}) = ∅ ∧ ({𝐴, 𝐵} ∩ {𝐷}) = ∅) ↔ ({𝐴, 𝐵} ∩ ({𝐶} ∪ {𝐷})) = ∅) |
63 | | df-pr 4570 |
. . . . . . . . 9
⊢ {𝐶, 𝐷} = ({𝐶} ∪ {𝐷}) |
64 | 63 | eqcomi 2749 |
. . . . . . . 8
⊢ ({𝐶} ∪ {𝐷}) = {𝐶, 𝐷} |
65 | 64 | ineq2i 4149 |
. . . . . . 7
⊢ ({𝐴, 𝐵} ∩ ({𝐶} ∪ {𝐷})) = ({𝐴, 𝐵} ∩ {𝐶, 𝐷}) |
66 | 65 | eqeq1i 2745 |
. . . . . 6
⊢ (({𝐴, 𝐵} ∩ ({𝐶} ∪ {𝐷})) = ∅ ↔ ({𝐴, 𝐵} ∩ {𝐶, 𝐷}) = ∅) |
67 | 62, 66 | bitri 274 |
. . . . 5
⊢ ((({𝐴, 𝐵} ∩ {𝐶}) = ∅ ∧ ({𝐴, 𝐵} ∩ {𝐷}) = ∅) ↔ ({𝐴, 𝐵} ∩ {𝐶, 𝐷}) = ∅) |
68 | 61, 67 | sylib 217 |
. . . 4
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌)) ∧ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷))) → ({𝐴, 𝐵} ∩ {𝐶, 𝐷}) = ∅) |
69 | | df-pr 4570 |
. . . . . . . . 9
⊢ {0, 1} =
({0} ∪ {1}) |
70 | 69 | eqcomi 2749 |
. . . . . . . 8
⊢ ({0}
∪ {1}) = {0, 1} |
71 | 70 | ineq1i 4148 |
. . . . . . 7
⊢ (({0}
∪ {1}) ∩ {2}) = ({0, 1} ∩ {2}) |
72 | | 0ne2 12180 |
. . . . . . . . . 10
⊢ 0 ≠
2 |
73 | | disjsn2 4654 |
. . . . . . . . . 10
⊢ (0 ≠ 2
→ ({0} ∩ {2}) = ∅) |
74 | 72, 73 | ax-mp 5 |
. . . . . . . . 9
⊢ ({0}
∩ {2}) = ∅ |
75 | | 1ne2 12181 |
. . . . . . . . . 10
⊢ 1 ≠
2 |
76 | | disjsn2 4654 |
. . . . . . . . . 10
⊢ (1 ≠ 2
→ ({1} ∩ {2}) = ∅) |
77 | 75, 76 | ax-mp 5 |
. . . . . . . . 9
⊢ ({1}
∩ {2}) = ∅ |
78 | 74, 77 | pm3.2i 471 |
. . . . . . . 8
⊢ (({0}
∩ {2}) = ∅ ∧ ({1} ∩ {2}) = ∅) |
79 | | undisj1 4401 |
. . . . . . . 8
⊢ ((({0}
∩ {2}) = ∅ ∧ ({1} ∩ {2}) = ∅) ↔ (({0} ∪ {1})
∩ {2}) = ∅) |
80 | 78, 79 | mpbi 229 |
. . . . . . 7
⊢ (({0}
∪ {1}) ∩ {2}) = ∅ |
81 | 71, 80 | eqtr3i 2770 |
. . . . . 6
⊢ ({0, 1}
∩ {2}) = ∅ |
82 | 70 | ineq1i 4148 |
. . . . . . 7
⊢ (({0}
∪ {1}) ∩ {3}) = ({0, 1} ∩ {3}) |
83 | | 3ne0 12079 |
. . . . . . . . . . 11
⊢ 3 ≠
0 |
84 | 83 | necomi 3000 |
. . . . . . . . . 10
⊢ 0 ≠
3 |
85 | | disjsn2 4654 |
. . . . . . . . . 10
⊢ (0 ≠ 3
→ ({0} ∩ {3}) = ∅) |
86 | 84, 85 | ax-mp 5 |
. . . . . . . . 9
⊢ ({0}
∩ {3}) = ∅ |
87 | | 1re 10976 |
. . . . . . . . . . 11
⊢ 1 ∈
ℝ |
88 | | 1lt3 12146 |
. . . . . . . . . . 11
⊢ 1 <
3 |
89 | 87, 88 | ltneii 11088 |
. . . . . . . . . 10
⊢ 1 ≠
3 |
90 | | disjsn2 4654 |
. . . . . . . . . 10
⊢ (1 ≠ 3
→ ({1} ∩ {3}) = ∅) |
91 | 89, 90 | ax-mp 5 |
. . . . . . . . 9
⊢ ({1}
∩ {3}) = ∅ |
92 | 86, 91 | pm3.2i 471 |
. . . . . . . 8
⊢ (({0}
∩ {3}) = ∅ ∧ ({1} ∩ {3}) = ∅) |
93 | | undisj1 4401 |
. . . . . . . 8
⊢ ((({0}
∩ {3}) = ∅ ∧ ({1} ∩ {3}) = ∅) ↔ (({0} ∪ {1})
∩ {3}) = ∅) |
94 | 92, 93 | mpbi 229 |
. . . . . . 7
⊢ (({0}
∪ {1}) ∩ {3}) = ∅ |
95 | 82, 94 | eqtr3i 2770 |
. . . . . 6
⊢ ({0, 1}
∩ {3}) = ∅ |
96 | 81, 95 | pm3.2i 471 |
. . . . 5
⊢ (({0, 1}
∩ {2}) = ∅ ∧ ({0, 1} ∩ {3}) = ∅) |
97 | | undisj2 4402 |
. . . . . 6
⊢ ((({0, 1}
∩ {2}) = ∅ ∧ ({0, 1} ∩ {3}) = ∅) ↔ ({0, 1} ∩
({2} ∪ {3})) = ∅) |
98 | | df-pr 4570 |
. . . . . . . . 9
⊢ {2, 3} =
({2} ∪ {3}) |
99 | 98 | eqcomi 2749 |
. . . . . . . 8
⊢ ({2}
∪ {3}) = {2, 3} |
100 | 99 | ineq2i 4149 |
. . . . . . 7
⊢ ({0, 1}
∩ ({2} ∪ {3})) = ({0, 1} ∩ {2, 3}) |
101 | 100 | eqeq1i 2745 |
. . . . . 6
⊢ (({0, 1}
∩ ({2} ∪ {3})) = ∅ ↔ ({0, 1} ∩ {2, 3}) =
∅) |
102 | 97, 101 | bitri 274 |
. . . . 5
⊢ ((({0, 1}
∩ {2}) = ∅ ∧ ({0, 1} ∩ {3}) = ∅) ↔ ({0, 1} ∩
{2, 3}) = ∅) |
103 | 96, 102 | mpbi 229 |
. . . 4
⊢ ({0, 1}
∩ {2, 3}) = ∅ |
104 | 68, 103 | jctil 520 |
. . 3
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌)) ∧ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷))) → (({0, 1} ∩ {2, 3}) = ∅
∧ ({𝐴, 𝐵} ∩ {𝐶, 𝐷}) = ∅)) |
105 | | f1oun 6733 |
. . 3
⊢
((({〈0, 𝐴〉, 〈1, 𝐵〉}:{0, 1}–1-1-onto→{𝐴, 𝐵} ∧ {〈2, 𝐶〉, 〈3, 𝐷〉}:{2, 3}–1-1-onto→{𝐶, 𝐷}) ∧ (({0, 1} ∩ {2, 3}) = ∅
∧ ({𝐴, 𝐵} ∩ {𝐶, 𝐷}) = ∅)) → ({〈0, 𝐴〉, 〈1, 𝐵〉} ∪ {〈2, 𝐶〉, 〈3, 𝐷〉}):({0, 1} ∪ {2,
3})–1-1-onto→({𝐴, 𝐵} ∪ {𝐶, 𝐷})) |
106 | 17, 37, 104, 105 | syl21anc 835 |
. 2
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌)) ∧ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷))) → ({〈0, 𝐴〉, 〈1, 𝐵〉} ∪ {〈2, 𝐶〉, 〈3, 𝐷〉}):({0, 1} ∪ {2, 3})–1-1-onto→({𝐴, 𝐵} ∪ {𝐶, 𝐷})) |
107 | 106 | ex 413 |
1
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌)) → (((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷)) → ({〈0, 𝐴〉, 〈1, 𝐵〉} ∪ {〈2, 𝐶〉, 〈3, 𝐷〉}):({0, 1} ∪ {2, 3})–1-1-onto→({𝐴, 𝐵} ∪ {𝐶, 𝐷}))) |