Proof of Theorem 2trllemE
Step | Hyp | Ref
| Expression |
1 | | c0ex 9913 |
. . . . . 6
⊢ 0 ∈
V |
2 | | 2trlX.i |
. . . . . . 7
⊢ (𝐼 ∈ 𝑈 ∧ 𝐽 ∈ 𝑊) |
3 | 2 | simpli 473 |
. . . . . 6
⊢ 𝐼 ∈ 𝑈 |
4 | 1, 3 | pm3.2i 470 |
. . . . 5
⊢ (0 ∈
V ∧ 𝐼 ∈ 𝑈) |
5 | | 1ex 9914 |
. . . . . 6
⊢ 1 ∈
V |
6 | 2 | simpri 477 |
. . . . . 6
⊢ 𝐽 ∈ 𝑊 |
7 | 5, 6 | pm3.2i 470 |
. . . . 5
⊢ (1 ∈
V ∧ 𝐽 ∈ 𝑊) |
8 | 4, 7 | pm3.2i 470 |
. . . 4
⊢ ((0
∈ V ∧ 𝐼 ∈
𝑈) ∧ (1 ∈ V ∧
𝐽 ∈ 𝑊)) |
9 | | simp2 1055 |
. . . . 5
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝐵 ∈ 𝑉) ∧ 𝐼 ≠ 𝐽 ∧ ((𝐸‘𝐼) = {𝐴, 𝐵} ∧ (𝐸‘𝐽) = {𝐵, 𝐶})) → 𝐼 ≠ 𝐽) |
10 | | 0ne1 10965 |
. . . . 5
⊢ 0 ≠
1 |
11 | 9, 10 | jctil 558 |
. . . 4
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝐵 ∈ 𝑉) ∧ 𝐼 ≠ 𝐽 ∧ ((𝐸‘𝐼) = {𝐴, 𝐵} ∧ (𝐸‘𝐽) = {𝐵, 𝐶})) → (0 ≠ 1 ∧ 𝐼 ≠ 𝐽)) |
12 | | f1oprg 6093 |
. . . 4
⊢ (((0
∈ V ∧ 𝐼 ∈
𝑈) ∧ (1 ∈ V ∧
𝐽 ∈ 𝑊)) → ((0 ≠ 1 ∧ 𝐼 ≠ 𝐽) → {〈0, 𝐼〉, 〈1, 𝐽〉}:{0, 1}–1-1-onto→{𝐼, 𝐽})) |
13 | 8, 11, 12 | mpsyl 66 |
. . 3
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝐵 ∈ 𝑉) ∧ 𝐼 ≠ 𝐽 ∧ ((𝐸‘𝐼) = {𝐴, 𝐵} ∧ (𝐸‘𝐽) = {𝐵, 𝐶})) → {〈0, 𝐼〉, 〈1, 𝐽〉}:{0, 1}–1-1-onto→{𝐼, 𝐽}) |
14 | | f1of1 6049 |
. . . 4
⊢
({〈0, 𝐼〉,
〈1, 𝐽〉}:{0,
1}–1-1-onto→{𝐼, 𝐽} → {〈0, 𝐼〉, 〈1, 𝐽〉}:{0, 1}–1-1→{𝐼, 𝐽}) |
15 | | 2trlX.f |
. . . . . . . . . . 11
⊢ 𝐹 = {〈0, 𝐼〉, 〈1, 𝐽〉} |
16 | 2, 15 | 2trllemB 26081 |
. . . . . . . . . 10
⊢
(0..^(#‘𝐹)) =
{0, 1} |
17 | 16 | eqcomi 2619 |
. . . . . . . . 9
⊢ {0, 1} =
(0..^(#‘𝐹)) |
18 | | f1eq2 6010 |
. . . . . . . . 9
⊢ ({0, 1} =
(0..^(#‘𝐹)) →
({〈0, 𝐼〉,
〈1, 𝐽〉}:{0,
1}–1-1→{𝐼, 𝐽} ↔ {〈0, 𝐼〉, 〈1, 𝐽〉}:(0..^(#‘𝐹))–1-1→{𝐼, 𝐽})) |
19 | 17, 18 | ax-mp 5 |
. . . . . . . 8
⊢
({〈0, 𝐼〉,
〈1, 𝐽〉}:{0,
1}–1-1→{𝐼, 𝐽} ↔ {〈0, 𝐼〉, 〈1, 𝐽〉}:(0..^(#‘𝐹))–1-1→{𝐼, 𝐽}) |
20 | 19 | biimpi 205 |
. . . . . . 7
⊢
({〈0, 𝐼〉,
〈1, 𝐽〉}:{0,
1}–1-1→{𝐼, 𝐽} → {〈0, 𝐼〉, 〈1, 𝐽〉}:(0..^(#‘𝐹))–1-1→{𝐼, 𝐽}) |
21 | 20 | adantr 480 |
. . . . . 6
⊢
(({〈0, 𝐼〉,
〈1, 𝐽〉}:{0,
1}–1-1→{𝐼, 𝐽} ∧ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝐵 ∈ 𝑉) ∧ 𝐼 ≠ 𝐽 ∧ ((𝐸‘𝐼) = {𝐴, 𝐵} ∧ (𝐸‘𝐽) = {𝐵, 𝐶}))) → {〈0, 𝐼〉, 〈1, 𝐽〉}:(0..^(#‘𝐹))–1-1→{𝐼, 𝐽}) |
22 | | 2trllemF 26079 |
. . . . . . . . . . . . . 14
⊢ (((𝐸‘𝐼) = {𝐴, 𝐵} ∧ 𝐵 ∈ 𝑉) → 𝐼 ∈ dom 𝐸) |
23 | 22 | adantlr 747 |
. . . . . . . . . . . . 13
⊢ ((((𝐸‘𝐼) = {𝐴, 𝐵} ∧ (𝐸‘𝐽) = {𝐵, 𝐶}) ∧ 𝐵 ∈ 𝑉) → 𝐼 ∈ dom 𝐸) |
24 | | prcom 4211 |
. . . . . . . . . . . . . . . . 17
⊢ {𝐵, 𝐶} = {𝐶, 𝐵} |
25 | 24 | eqeq2i 2622 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐸‘𝐽) = {𝐵, 𝐶} ↔ (𝐸‘𝐽) = {𝐶, 𝐵}) |
26 | 25 | biimpi 205 |
. . . . . . . . . . . . . . 15
⊢ ((𝐸‘𝐽) = {𝐵, 𝐶} → (𝐸‘𝐽) = {𝐶, 𝐵}) |
27 | 26 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ (((𝐸‘𝐼) = {𝐴, 𝐵} ∧ (𝐸‘𝐽) = {𝐵, 𝐶}) → (𝐸‘𝐽) = {𝐶, 𝐵}) |
28 | | 2trllemF 26079 |
. . . . . . . . . . . . . 14
⊢ (((𝐸‘𝐽) = {𝐶, 𝐵} ∧ 𝐵 ∈ 𝑉) → 𝐽 ∈ dom 𝐸) |
29 | 27, 28 | sylan 487 |
. . . . . . . . . . . . 13
⊢ ((((𝐸‘𝐼) = {𝐴, 𝐵} ∧ (𝐸‘𝐽) = {𝐵, 𝐶}) ∧ 𝐵 ∈ 𝑉) → 𝐽 ∈ dom 𝐸) |
30 | 23, 29 | jca 553 |
. . . . . . . . . . . 12
⊢ ((((𝐸‘𝐼) = {𝐴, 𝐵} ∧ (𝐸‘𝐽) = {𝐵, 𝐶}) ∧ 𝐵 ∈ 𝑉) → (𝐼 ∈ dom 𝐸 ∧ 𝐽 ∈ dom 𝐸)) |
31 | 30 | expcom 450 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ 𝑉 → (((𝐸‘𝐼) = {𝐴, 𝐵} ∧ (𝐸‘𝐽) = {𝐵, 𝐶}) → (𝐼 ∈ dom 𝐸 ∧ 𝐽 ∈ dom 𝐸))) |
32 | 31 | 3ad2ant3 1077 |
. . . . . . . . . 10
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝐵 ∈ 𝑉) → (((𝐸‘𝐼) = {𝐴, 𝐵} ∧ (𝐸‘𝐽) = {𝐵, 𝐶}) → (𝐼 ∈ dom 𝐸 ∧ 𝐽 ∈ dom 𝐸))) |
33 | 32 | imp 444 |
. . . . . . . . 9
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝐵 ∈ 𝑉) ∧ ((𝐸‘𝐼) = {𝐴, 𝐵} ∧ (𝐸‘𝐽) = {𝐵, 𝐶})) → (𝐼 ∈ dom 𝐸 ∧ 𝐽 ∈ dom 𝐸)) |
34 | 33 | 3adant2 1073 |
. . . . . . . 8
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝐵 ∈ 𝑉) ∧ 𝐼 ≠ 𝐽 ∧ ((𝐸‘𝐼) = {𝐴, 𝐵} ∧ (𝐸‘𝐽) = {𝐵, 𝐶})) → (𝐼 ∈ dom 𝐸 ∧ 𝐽 ∈ dom 𝐸)) |
35 | 34 | adantl 481 |
. . . . . . 7
⊢
(({〈0, 𝐼〉,
〈1, 𝐽〉}:{0,
1}–1-1→{𝐼, 𝐽} ∧ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝐵 ∈ 𝑉) ∧ 𝐼 ≠ 𝐽 ∧ ((𝐸‘𝐼) = {𝐴, 𝐵} ∧ (𝐸‘𝐽) = {𝐵, 𝐶}))) → (𝐼 ∈ dom 𝐸 ∧ 𝐽 ∈ dom 𝐸)) |
36 | | prssg 4290 |
. . . . . . . 8
⊢ ((𝐼 ∈ 𝑈 ∧ 𝐽 ∈ 𝑊) → ((𝐼 ∈ dom 𝐸 ∧ 𝐽 ∈ dom 𝐸) ↔ {𝐼, 𝐽} ⊆ dom 𝐸)) |
37 | 2, 36 | ax-mp 5 |
. . . . . . 7
⊢ ((𝐼 ∈ dom 𝐸 ∧ 𝐽 ∈ dom 𝐸) ↔ {𝐼, 𝐽} ⊆ dom 𝐸) |
38 | 35, 37 | sylib 207 |
. . . . . 6
⊢
(({〈0, 𝐼〉,
〈1, 𝐽〉}:{0,
1}–1-1→{𝐼, 𝐽} ∧ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝐵 ∈ 𝑉) ∧ 𝐼 ≠ 𝐽 ∧ ((𝐸‘𝐼) = {𝐴, 𝐵} ∧ (𝐸‘𝐽) = {𝐵, 𝐶}))) → {𝐼, 𝐽} ⊆ dom 𝐸) |
39 | | f1ss 6019 |
. . . . . 6
⊢
(({〈0, 𝐼〉,
〈1, 𝐽〉}:(0..^(#‘𝐹))–1-1→{𝐼, 𝐽} ∧ {𝐼, 𝐽} ⊆ dom 𝐸) → {〈0, 𝐼〉, 〈1, 𝐽〉}:(0..^(#‘𝐹))–1-1→dom 𝐸) |
40 | 21, 38, 39 | syl2anc 691 |
. . . . 5
⊢
(({〈0, 𝐼〉,
〈1, 𝐽〉}:{0,
1}–1-1→{𝐼, 𝐽} ∧ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝐵 ∈ 𝑉) ∧ 𝐼 ≠ 𝐽 ∧ ((𝐸‘𝐼) = {𝐴, 𝐵} ∧ (𝐸‘𝐽) = {𝐵, 𝐶}))) → {〈0, 𝐼〉, 〈1, 𝐽〉}:(0..^(#‘𝐹))–1-1→dom 𝐸) |
41 | 40 | ex 449 |
. . . 4
⊢
({〈0, 𝐼〉,
〈1, 𝐽〉}:{0,
1}–1-1→{𝐼, 𝐽} → (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝐵 ∈ 𝑉) ∧ 𝐼 ≠ 𝐽 ∧ ((𝐸‘𝐼) = {𝐴, 𝐵} ∧ (𝐸‘𝐽) = {𝐵, 𝐶})) → {〈0, 𝐼〉, 〈1, 𝐽〉}:(0..^(#‘𝐹))–1-1→dom 𝐸)) |
42 | 14, 41 | syl 17 |
. . 3
⊢
({〈0, 𝐼〉,
〈1, 𝐽〉}:{0,
1}–1-1-onto→{𝐼, 𝐽} → (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝐵 ∈ 𝑉) ∧ 𝐼 ≠ 𝐽 ∧ ((𝐸‘𝐼) = {𝐴, 𝐵} ∧ (𝐸‘𝐽) = {𝐵, 𝐶})) → {〈0, 𝐼〉, 〈1, 𝐽〉}:(0..^(#‘𝐹))–1-1→dom 𝐸)) |
43 | 13, 42 | mpcom 37 |
. 2
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝐵 ∈ 𝑉) ∧ 𝐼 ≠ 𝐽 ∧ ((𝐸‘𝐼) = {𝐴, 𝐵} ∧ (𝐸‘𝐽) = {𝐵, 𝐶})) → {〈0, 𝐼〉, 〈1, 𝐽〉}:(0..^(#‘𝐹))–1-1→dom 𝐸) |
44 | | f1eq1 6009 |
. . 3
⊢ (𝐹 = {〈0, 𝐼〉, 〈1, 𝐽〉} → (𝐹:(0..^(#‘𝐹))–1-1→dom 𝐸 ↔ {〈0, 𝐼〉, 〈1, 𝐽〉}:(0..^(#‘𝐹))–1-1→dom 𝐸)) |
45 | 15, 44 | ax-mp 5 |
. 2
⊢ (𝐹:(0..^(#‘𝐹))–1-1→dom 𝐸 ↔ {〈0, 𝐼〉, 〈1, 𝐽〉}:(0..^(#‘𝐹))–1-1→dom 𝐸) |
46 | 43, 45 | sylibr 223 |
1
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝐵 ∈ 𝑉) ∧ 𝐼 ≠ 𝐽 ∧ ((𝐸‘𝐼) = {𝐴, 𝐵} ∧ (𝐸‘𝐽) = {𝐵, 𝐶})) → 𝐹:(0..^(#‘𝐹))–1-1→dom 𝐸) |