Step | Hyp | Ref
| Expression |
1 | | f1oun2prg 14628 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → (((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷)) → ({〈0, 𝐴〉, 〈1, 𝐵〉} ∪ {〈2, 𝐶〉, 〈3, 𝐷〉}):({0, 1} ∪ {2, 3})–1-1-onto→({𝐴, 𝐵} ∪ {𝐶, 𝐷}))) |
2 | 1 | imp 407 |
. . . . 5
⊢ ((((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) ∧ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷))) → ({〈0, 𝐴〉, 〈1, 𝐵〉} ∪ {〈2, 𝐶〉, 〈3, 𝐷〉}):({0, 1} ∪ {2, 3})–1-1-onto→({𝐴, 𝐵} ∪ {𝐶, 𝐷})) |
3 | 2 | adantr 481 |
. . . 4
⊢
(((((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) ∧ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷))) ∧ 𝐸 = 〈“𝐴𝐵𝐶𝐷”〉) → ({〈0, 𝐴〉, 〈1, 𝐵〉} ∪ {〈2, 𝐶〉, 〈3, 𝐷〉}):({0, 1} ∪ {2,
3})–1-1-onto→({𝐴, 𝐵} ∪ {𝐶, 𝐷})) |
4 | | s4prop 14621 |
. . . . . . . . 9
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → 〈“𝐴𝐵𝐶𝐷”〉 = ({〈0, 𝐴〉, 〈1, 𝐵〉} ∪ {〈2, 𝐶〉, 〈3, 𝐷〉})) |
5 | 4 | adantr 481 |
. . . . . . . 8
⊢ ((((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) ∧ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷))) → 〈“𝐴𝐵𝐶𝐷”〉 = ({〈0, 𝐴〉, 〈1, 𝐵〉} ∪ {〈2, 𝐶〉, 〈3, 𝐷〉})) |
6 | 5 | eqeq2d 2751 |
. . . . . . 7
⊢ ((((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) ∧ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷))) → (𝐸 = 〈“𝐴𝐵𝐶𝐷”〉 ↔ 𝐸 = ({〈0, 𝐴〉, 〈1, 𝐵〉} ∪ {〈2, 𝐶〉, 〈3, 𝐷〉}))) |
7 | 6 | biimpa 477 |
. . . . . 6
⊢
(((((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) ∧ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷))) ∧ 𝐸 = 〈“𝐴𝐵𝐶𝐷”〉) → 𝐸 = ({〈0, 𝐴〉, 〈1, 𝐵〉} ∪ {〈2, 𝐶〉, 〈3, 𝐷〉})) |
8 | 7 | eqcomd 2746 |
. . . . 5
⊢
(((((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) ∧ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷))) ∧ 𝐸 = 〈“𝐴𝐵𝐶𝐷”〉) → ({〈0, 𝐴〉, 〈1, 𝐵〉} ∪ {〈2, 𝐶〉, 〈3, 𝐷〉}) = 𝐸) |
9 | 8 | f1oeq1d 6709 |
. . . 4
⊢
(((((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) ∧ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷))) ∧ 𝐸 = 〈“𝐴𝐵𝐶𝐷”〉) → (({〈0, 𝐴〉, 〈1, 𝐵〉} ∪ {〈2, 𝐶〉, 〈3, 𝐷〉}):({0, 1} ∪ {2,
3})–1-1-onto→({𝐴, 𝐵} ∪ {𝐶, 𝐷}) ↔ 𝐸:({0, 1} ∪ {2, 3})–1-1-onto→({𝐴, 𝐵} ∪ {𝐶, 𝐷}))) |
10 | 3, 9 | mpbid 231 |
. . 3
⊢
(((((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) ∧ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷))) ∧ 𝐸 = 〈“𝐴𝐵𝐶𝐷”〉) → 𝐸:({0, 1} ∪ {2, 3})–1-1-onto→({𝐴, 𝐵} ∪ {𝐶, 𝐷})) |
11 | | dff1o5 6723 |
. . . . . . 7
⊢ (𝐸:({0, 1} ∪ {2,
3})–1-1-onto→({𝐴, 𝐵} ∪ {𝐶, 𝐷}) ↔ (𝐸:({0, 1} ∪ {2, 3})–1-1→({𝐴, 𝐵} ∪ {𝐶, 𝐷}) ∧ ran 𝐸 = ({𝐴, 𝐵} ∪ {𝐶, 𝐷}))) |
12 | | dff12 6667 |
. . . . . . . . 9
⊢ (𝐸:({0, 1} ∪ {2,
3})–1-1→({𝐴, 𝐵} ∪ {𝐶, 𝐷}) ↔ (𝐸:({0, 1} ∪ {2, 3})⟶({𝐴, 𝐵} ∪ {𝐶, 𝐷}) ∧ ∀𝑦∃*𝑥 𝑥𝐸𝑦)) |
13 | 12 | bicomi 223 |
. . . . . . . 8
⊢ ((𝐸:({0, 1} ∪ {2,
3})⟶({𝐴, 𝐵} ∪ {𝐶, 𝐷}) ∧ ∀𝑦∃*𝑥 𝑥𝐸𝑦) ↔ 𝐸:({0, 1} ∪ {2, 3})–1-1→({𝐴, 𝐵} ∪ {𝐶, 𝐷})) |
14 | 13 | anbi1i 624 |
. . . . . . 7
⊢ (((𝐸:({0, 1} ∪ {2,
3})⟶({𝐴, 𝐵} ∪ {𝐶, 𝐷}) ∧ ∀𝑦∃*𝑥 𝑥𝐸𝑦) ∧ ran 𝐸 = ({𝐴, 𝐵} ∪ {𝐶, 𝐷})) ↔ (𝐸:({0, 1} ∪ {2, 3})–1-1→({𝐴, 𝐵} ∪ {𝐶, 𝐷}) ∧ ran 𝐸 = ({𝐴, 𝐵} ∪ {𝐶, 𝐷}))) |
15 | 11, 14 | sylbb2 237 |
. . . . . 6
⊢ (𝐸:({0, 1} ∪ {2,
3})–1-1-onto→({𝐴, 𝐵} ∪ {𝐶, 𝐷}) → ((𝐸:({0, 1} ∪ {2, 3})⟶({𝐴, 𝐵} ∪ {𝐶, 𝐷}) ∧ ∀𝑦∃*𝑥 𝑥𝐸𝑦) ∧ ran 𝐸 = ({𝐴, 𝐵} ∪ {𝐶, 𝐷}))) |
16 | | ffdm 6628 |
. . . . . . . . 9
⊢ (𝐸:({0, 1} ∪ {2,
3})⟶({𝐴, 𝐵} ∪ {𝐶, 𝐷}) → (𝐸:dom 𝐸⟶({𝐴, 𝐵} ∪ {𝐶, 𝐷}) ∧ dom 𝐸 ⊆ ({0, 1} ∪ {2,
3}))) |
17 | 16 | simpld 495 |
. . . . . . . 8
⊢ (𝐸:({0, 1} ∪ {2,
3})⟶({𝐴, 𝐵} ∪ {𝐶, 𝐷}) → 𝐸:dom 𝐸⟶({𝐴, 𝐵} ∪ {𝐶, 𝐷})) |
18 | 17 | anim1i 615 |
. . . . . . 7
⊢ ((𝐸:({0, 1} ∪ {2,
3})⟶({𝐴, 𝐵} ∪ {𝐶, 𝐷}) ∧ ∀𝑦∃*𝑥 𝑥𝐸𝑦) → (𝐸:dom 𝐸⟶({𝐴, 𝐵} ∪ {𝐶, 𝐷}) ∧ ∀𝑦∃*𝑥 𝑥𝐸𝑦)) |
19 | 18 | anim1i 615 |
. . . . . 6
⊢ (((𝐸:({0, 1} ∪ {2,
3})⟶({𝐴, 𝐵} ∪ {𝐶, 𝐷}) ∧ ∀𝑦∃*𝑥 𝑥𝐸𝑦) ∧ ran 𝐸 = ({𝐴, 𝐵} ∪ {𝐶, 𝐷})) → ((𝐸:dom 𝐸⟶({𝐴, 𝐵} ∪ {𝐶, 𝐷}) ∧ ∀𝑦∃*𝑥 𝑥𝐸𝑦) ∧ ran 𝐸 = ({𝐴, 𝐵} ∪ {𝐶, 𝐷}))) |
20 | 15, 19 | syl 17 |
. . . . 5
⊢ (𝐸:({0, 1} ∪ {2,
3})–1-1-onto→({𝐴, 𝐵} ∪ {𝐶, 𝐷}) → ((𝐸:dom 𝐸⟶({𝐴, 𝐵} ∪ {𝐶, 𝐷}) ∧ ∀𝑦∃*𝑥 𝑥𝐸𝑦) ∧ ran 𝐸 = ({𝐴, 𝐵} ∪ {𝐶, 𝐷}))) |
21 | | dff12 6667 |
. . . . . 6
⊢ (𝐸:dom 𝐸–1-1→({𝐴, 𝐵} ∪ {𝐶, 𝐷}) ↔ (𝐸:dom 𝐸⟶({𝐴, 𝐵} ∪ {𝐶, 𝐷}) ∧ ∀𝑦∃*𝑥 𝑥𝐸𝑦)) |
22 | 21 | anbi1i 624 |
. . . . 5
⊢ ((𝐸:dom 𝐸–1-1→({𝐴, 𝐵} ∪ {𝐶, 𝐷}) ∧ ran 𝐸 = ({𝐴, 𝐵} ∪ {𝐶, 𝐷})) ↔ ((𝐸:dom 𝐸⟶({𝐴, 𝐵} ∪ {𝐶, 𝐷}) ∧ ∀𝑦∃*𝑥 𝑥𝐸𝑦) ∧ ran 𝐸 = ({𝐴, 𝐵} ∪ {𝐶, 𝐷}))) |
23 | 20, 22 | sylibr 233 |
. . . 4
⊢ (𝐸:({0, 1} ∪ {2,
3})–1-1-onto→({𝐴, 𝐵} ∪ {𝐶, 𝐷}) → (𝐸:dom 𝐸–1-1→({𝐴, 𝐵} ∪ {𝐶, 𝐷}) ∧ ran 𝐸 = ({𝐴, 𝐵} ∪ {𝐶, 𝐷}))) |
24 | | dff1o5 6723 |
. . . 4
⊢ (𝐸:dom 𝐸–1-1-onto→({𝐴, 𝐵} ∪ {𝐶, 𝐷}) ↔ (𝐸:dom 𝐸–1-1→({𝐴, 𝐵} ∪ {𝐶, 𝐷}) ∧ ran 𝐸 = ({𝐴, 𝐵} ∪ {𝐶, 𝐷}))) |
25 | 23, 24 | sylibr 233 |
. . 3
⊢ (𝐸:({0, 1} ∪ {2,
3})–1-1-onto→({𝐴, 𝐵} ∪ {𝐶, 𝐷}) → 𝐸:dom 𝐸–1-1-onto→({𝐴, 𝐵} ∪ {𝐶, 𝐷})) |
26 | 10, 25 | syl 17 |
. 2
⊢
(((((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) ∧ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷))) ∧ 𝐸 = 〈“𝐴𝐵𝐶𝐷”〉) → 𝐸:dom 𝐸–1-1-onto→({𝐴, 𝐵} ∪ {𝐶, 𝐷})) |
27 | 26 | exp31 420 |
1
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → (((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷)) → (𝐸 = 〈“𝐴𝐵𝐶𝐷”〉 → 𝐸:dom 𝐸–1-1-onto→({𝐴, 𝐵} ∪ {𝐶, 𝐷})))) |