| Step |
Hyp |
Ref |
Expression |
| 1 |
|
usgr2pthlem.v |
⊢ 𝑉 = ( Vtx ‘ 𝐺 ) |
| 2 |
|
usgr2pthlem.i |
⊢ 𝐼 = ( iEdg ‘ 𝐺 ) |
| 3 |
|
0nn0 |
⊢ 0 ∈ ℕ0 |
| 4 |
|
2nn0 |
⊢ 2 ∈ ℕ0 |
| 5 |
|
0le2 |
⊢ 0 ≤ 2 |
| 6 |
|
elfz2nn0 |
⊢ ( 0 ∈ ( 0 ... 2 ) ↔ ( 0 ∈ ℕ0 ∧ 2 ∈ ℕ0 ∧ 0 ≤ 2 ) ) |
| 7 |
3 4 5 6
|
mpbir3an |
⊢ 0 ∈ ( 0 ... 2 ) |
| 8 |
|
ffvelcdm |
⊢ ( ( 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ∧ 0 ∈ ( 0 ... 2 ) ) → ( 𝑃 ‘ 0 ) ∈ 𝑉 ) |
| 9 |
7 8
|
mpan2 |
⊢ ( 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 → ( 𝑃 ‘ 0 ) ∈ 𝑉 ) |
| 10 |
9
|
adantl |
⊢ ( ( ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ∧ 𝐺 ∈ USGraph ) ∧ 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ) → ( 𝑃 ‘ 0 ) ∈ 𝑉 ) |
| 11 |
|
1nn0 |
⊢ 1 ∈ ℕ0 |
| 12 |
|
1le2 |
⊢ 1 ≤ 2 |
| 13 |
|
elfz2nn0 |
⊢ ( 1 ∈ ( 0 ... 2 ) ↔ ( 1 ∈ ℕ0 ∧ 2 ∈ ℕ0 ∧ 1 ≤ 2 ) ) |
| 14 |
11 4 12 13
|
mpbir3an |
⊢ 1 ∈ ( 0 ... 2 ) |
| 15 |
|
ffvelcdm |
⊢ ( ( 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ∧ 1 ∈ ( 0 ... 2 ) ) → ( 𝑃 ‘ 1 ) ∈ 𝑉 ) |
| 16 |
14 15
|
mpan2 |
⊢ ( 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 → ( 𝑃 ‘ 1 ) ∈ 𝑉 ) |
| 17 |
16
|
adantl |
⊢ ( ( ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ∧ 𝐺 ∈ USGraph ) ∧ 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ) → ( 𝑃 ‘ 1 ) ∈ 𝑉 ) |
| 18 |
|
simpr |
⊢ ( ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ∧ 𝐺 ∈ USGraph ) → 𝐺 ∈ USGraph ) |
| 19 |
|
fvex |
⊢ ( 𝑃 ‘ 1 ) ∈ V |
| 20 |
18 19
|
jctir |
⊢ ( ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ∧ 𝐺 ∈ USGraph ) → ( 𝐺 ∈ USGraph ∧ ( 𝑃 ‘ 1 ) ∈ V ) ) |
| 21 |
|
prcom |
⊢ { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 0 ) } |
| 22 |
21
|
eqeq2i |
⊢ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ↔ ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 0 ) } ) |
| 23 |
22
|
birani |
⊢ ( ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) → ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 0 ) } ) |
| 24 |
23
|
ad2antlr |
⊢ ( ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ∧ 𝐺 ∈ USGraph ) → ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 0 ) } ) |
| 25 |
2
|
usgrnloopv |
⊢ ( ( 𝐺 ∈ USGraph ∧ ( 𝑃 ‘ 1 ) ∈ V ) → ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 0 ) } → ( 𝑃 ‘ 1 ) ≠ ( 𝑃 ‘ 0 ) ) ) |
| 26 |
20 24 25
|
sylc |
⊢ ( ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ∧ 𝐺 ∈ USGraph ) → ( 𝑃 ‘ 1 ) ≠ ( 𝑃 ‘ 0 ) ) |
| 27 |
26
|
adantr |
⊢ ( ( ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ∧ 𝐺 ∈ USGraph ) ∧ 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ) → ( 𝑃 ‘ 1 ) ≠ ( 𝑃 ‘ 0 ) ) |
| 28 |
19
|
elsn |
⊢ ( ( 𝑃 ‘ 1 ) ∈ { ( 𝑃 ‘ 0 ) } ↔ ( 𝑃 ‘ 1 ) = ( 𝑃 ‘ 0 ) ) |
| 29 |
28
|
necon3bbii |
⊢ ( ¬ ( 𝑃 ‘ 1 ) ∈ { ( 𝑃 ‘ 0 ) } ↔ ( 𝑃 ‘ 1 ) ≠ ( 𝑃 ‘ 0 ) ) |
| 30 |
27 29
|
sylibr |
⊢ ( ( ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ∧ 𝐺 ∈ USGraph ) ∧ 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ) → ¬ ( 𝑃 ‘ 1 ) ∈ { ( 𝑃 ‘ 0 ) } ) |
| 31 |
17 30
|
eldifd |
⊢ ( ( ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ∧ 𝐺 ∈ USGraph ) ∧ 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ) → ( 𝑃 ‘ 1 ) ∈ ( 𝑉 ∖ { ( 𝑃 ‘ 0 ) } ) ) |
| 32 |
31
|
adantr |
⊢ ( ( ( ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ∧ 𝐺 ∈ USGraph ) ∧ 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ) ∧ 𝑥 = ( 𝑃 ‘ 0 ) ) → ( 𝑃 ‘ 1 ) ∈ ( 𝑉 ∖ { ( 𝑃 ‘ 0 ) } ) ) |
| 33 |
|
sneq |
⊢ ( 𝑥 = ( 𝑃 ‘ 0 ) → { 𝑥 } = { ( 𝑃 ‘ 0 ) } ) |
| 34 |
33
|
difeq2d |
⊢ ( 𝑥 = ( 𝑃 ‘ 0 ) → ( 𝑉 ∖ { 𝑥 } ) = ( 𝑉 ∖ { ( 𝑃 ‘ 0 ) } ) ) |
| 35 |
34
|
eleq2d |
⊢ ( 𝑥 = ( 𝑃 ‘ 0 ) → ( ( 𝑃 ‘ 1 ) ∈ ( 𝑉 ∖ { 𝑥 } ) ↔ ( 𝑃 ‘ 1 ) ∈ ( 𝑉 ∖ { ( 𝑃 ‘ 0 ) } ) ) ) |
| 36 |
35
|
adantl |
⊢ ( ( ( ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ∧ 𝐺 ∈ USGraph ) ∧ 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ) ∧ 𝑥 = ( 𝑃 ‘ 0 ) ) → ( ( 𝑃 ‘ 1 ) ∈ ( 𝑉 ∖ { 𝑥 } ) ↔ ( 𝑃 ‘ 1 ) ∈ ( 𝑉 ∖ { ( 𝑃 ‘ 0 ) } ) ) ) |
| 37 |
32 36
|
mpbird |
⊢ ( ( ( ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ∧ 𝐺 ∈ USGraph ) ∧ 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ) ∧ 𝑥 = ( 𝑃 ‘ 0 ) ) → ( 𝑃 ‘ 1 ) ∈ ( 𝑉 ∖ { 𝑥 } ) ) |
| 38 |
|
2re |
⊢ 2 ∈ ℝ |
| 39 |
38
|
leidi |
⊢ 2 ≤ 2 |
| 40 |
|
elfz2nn0 |
⊢ ( 2 ∈ ( 0 ... 2 ) ↔ ( 2 ∈ ℕ0 ∧ 2 ∈ ℕ0 ∧ 2 ≤ 2 ) ) |
| 41 |
4 4 39 40
|
mpbir3an |
⊢ 2 ∈ ( 0 ... 2 ) |
| 42 |
|
ffvelcdm |
⊢ ( ( 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ∧ 2 ∈ ( 0 ... 2 ) ) → ( 𝑃 ‘ 2 ) ∈ 𝑉 ) |
| 43 |
41 42
|
mpan2 |
⊢ ( 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 → ( 𝑃 ‘ 2 ) ∈ 𝑉 ) |
| 44 |
43
|
adantl |
⊢ ( ( ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ∧ 𝐺 ∈ USGraph ) ∧ 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ) → ( 𝑃 ‘ 2 ) ∈ 𝑉 ) |
| 45 |
2
|
usgrf1 |
⊢ ( 𝐺 ∈ USGraph → 𝐼 : dom 𝐼 –1-1→ ran 𝐼 ) |
| 46 |
45
|
ad2antlr |
⊢ ( ( ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ∧ 𝐺 ∈ USGraph ) ∧ 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ) → 𝐼 : dom 𝐼 –1-1→ ran 𝐼 ) |
| 47 |
|
simpl |
⊢ ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) → 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ) |
| 48 |
47
|
ad2antrr |
⊢ ( ( ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ∧ 𝐺 ∈ USGraph ) ∧ 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ) → 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ) |
| 49 |
46 48
|
jca |
⊢ ( ( ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ∧ 𝐺 ∈ USGraph ) ∧ 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ) → ( 𝐼 : dom 𝐼 –1-1→ ran 𝐼 ∧ 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ) ) |
| 50 |
|
2nn |
⊢ 2 ∈ ℕ |
| 51 |
|
lbfzo0 |
⊢ ( 0 ∈ ( 0 ..^ 2 ) ↔ 2 ∈ ℕ ) |
| 52 |
50 51
|
mpbir |
⊢ 0 ∈ ( 0 ..^ 2 ) |
| 53 |
|
1lt2 |
⊢ 1 < 2 |
| 54 |
|
elfzo0 |
⊢ ( 1 ∈ ( 0 ..^ 2 ) ↔ ( 1 ∈ ℕ0 ∧ 2 ∈ ℕ ∧ 1 < 2 ) ) |
| 55 |
11 50 53 54
|
mpbir3an |
⊢ 1 ∈ ( 0 ..^ 2 ) |
| 56 |
52 55
|
pm3.2i |
⊢ ( 0 ∈ ( 0 ..^ 2 ) ∧ 1 ∈ ( 0 ..^ 2 ) ) |
| 57 |
56
|
a1i |
⊢ ( ( ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ∧ 𝐺 ∈ USGraph ) ∧ 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ) → ( 0 ∈ ( 0 ..^ 2 ) ∧ 1 ∈ ( 0 ..^ 2 ) ) ) |
| 58 |
|
0ne1 |
⊢ 0 ≠ 1 |
| 59 |
58
|
a1i |
⊢ ( ( ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ∧ 𝐺 ∈ USGraph ) ∧ 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ) → 0 ≠ 1 ) |
| 60 |
49 57 59
|
3jca |
⊢ ( ( ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ∧ 𝐺 ∈ USGraph ) ∧ 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ) → ( ( 𝐼 : dom 𝐼 –1-1→ ran 𝐼 ∧ 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ) ∧ ( 0 ∈ ( 0 ..^ 2 ) ∧ 1 ∈ ( 0 ..^ 2 ) ) ∧ 0 ≠ 1 ) ) |
| 61 |
|
simpr |
⊢ ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) → ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) |
| 62 |
61
|
ad2antrr |
⊢ ( ( ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ∧ 𝐺 ∈ USGraph ) ∧ 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ) → ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) |
| 63 |
|
2f1fvneq |
⊢ ( ( ( 𝐼 : dom 𝐼 –1-1→ ran 𝐼 ∧ 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ) ∧ ( 0 ∈ ( 0 ..^ 2 ) ∧ 1 ∈ ( 0 ..^ 2 ) ) ∧ 0 ≠ 1 ) → ( ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) → { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ≠ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) |
| 64 |
60 62 63
|
sylc |
⊢ ( ( ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ∧ 𝐺 ∈ USGraph ) ∧ 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ) → { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ≠ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) |
| 65 |
|
necom |
⊢ ( ( 𝑃 ‘ 2 ) ≠ ( 𝑃 ‘ 0 ) ↔ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ) |
| 66 |
|
fvex |
⊢ ( 𝑃 ‘ 0 ) ∈ V |
| 67 |
|
fvex |
⊢ ( 𝑃 ‘ 2 ) ∈ V |
| 68 |
66 19 67
|
3pm3.2i |
⊢ ( ( 𝑃 ‘ 0 ) ∈ V ∧ ( 𝑃 ‘ 1 ) ∈ V ∧ ( 𝑃 ‘ 2 ) ∈ V ) |
| 69 |
|
fvexd |
⊢ ( ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ∧ 𝐺 ∈ USGraph ) → ( 𝑃 ‘ 0 ) ∈ V ) |
| 70 |
|
simpl |
⊢ ( ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) → ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ) |
| 71 |
70
|
ad2antlr |
⊢ ( ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ∧ 𝐺 ∈ USGraph ) → ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ) |
| 72 |
18 69 71
|
jca31 |
⊢ ( ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ∧ 𝐺 ∈ USGraph ) → ( ( 𝐺 ∈ USGraph ∧ ( 𝑃 ‘ 0 ) ∈ V ) ∧ ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ) ) |
| 73 |
72
|
adantr |
⊢ ( ( ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ∧ 𝐺 ∈ USGraph ) ∧ 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ) → ( ( 𝐺 ∈ USGraph ∧ ( 𝑃 ‘ 0 ) ∈ V ) ∧ ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ) ) |
| 74 |
2
|
usgrnloopv |
⊢ ( ( 𝐺 ∈ USGraph ∧ ( 𝑃 ‘ 0 ) ∈ V ) → ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ) ) |
| 75 |
74
|
imp |
⊢ ( ( ( 𝐺 ∈ USGraph ∧ ( 𝑃 ‘ 0 ) ∈ V ) ∧ ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ) → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ) |
| 76 |
73 75
|
syl |
⊢ ( ( ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ∧ 𝐺 ∈ USGraph ) ∧ 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ) → ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ) |
| 77 |
|
pr1nebg |
⊢ ( ( ( ( 𝑃 ‘ 0 ) ∈ V ∧ ( 𝑃 ‘ 1 ) ∈ V ∧ ( 𝑃 ‘ 2 ) ∈ V ) ∧ ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 1 ) ) → ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ↔ { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ≠ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) |
| 78 |
68 76 77
|
sylancr |
⊢ ( ( ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ∧ 𝐺 ∈ USGraph ) ∧ 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ) → ( ( 𝑃 ‘ 0 ) ≠ ( 𝑃 ‘ 2 ) ↔ { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ≠ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) |
| 79 |
65 78
|
bitrid |
⊢ ( ( ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ∧ 𝐺 ∈ USGraph ) ∧ 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ) → ( ( 𝑃 ‘ 2 ) ≠ ( 𝑃 ‘ 0 ) ↔ { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ≠ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) |
| 80 |
64 79
|
mpbird |
⊢ ( ( ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ∧ 𝐺 ∈ USGraph ) ∧ 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ) → ( 𝑃 ‘ 2 ) ≠ ( 𝑃 ‘ 0 ) ) |
| 81 |
|
fvexd |
⊢ ( ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ∧ 𝐺 ∈ USGraph ) → ( 𝑃 ‘ 2 ) ∈ V ) |
| 82 |
|
prcom |
⊢ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } = { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 1 ) } |
| 83 |
82
|
eqeq2i |
⊢ ( ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ↔ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 1 ) } ) |
| 84 |
83
|
bilani |
⊢ ( ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) → ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 1 ) } ) |
| 85 |
84
|
ad2antlr |
⊢ ( ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ∧ 𝐺 ∈ USGraph ) → ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 1 ) } ) |
| 86 |
18 81 85
|
jca31 |
⊢ ( ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ∧ 𝐺 ∈ USGraph ) → ( ( 𝐺 ∈ USGraph ∧ ( 𝑃 ‘ 2 ) ∈ V ) ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 1 ) } ) ) |
| 87 |
86
|
adantr |
⊢ ( ( ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ∧ 𝐺 ∈ USGraph ) ∧ 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ) → ( ( 𝐺 ∈ USGraph ∧ ( 𝑃 ‘ 2 ) ∈ V ) ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 1 ) } ) ) |
| 88 |
2
|
usgrnloopv |
⊢ ( ( 𝐺 ∈ USGraph ∧ ( 𝑃 ‘ 2 ) ∈ V ) → ( ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 1 ) } → ( 𝑃 ‘ 2 ) ≠ ( 𝑃 ‘ 1 ) ) ) |
| 89 |
88
|
imp |
⊢ ( ( ( 𝐺 ∈ USGraph ∧ ( 𝑃 ‘ 2 ) ∈ V ) ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 2 ) , ( 𝑃 ‘ 1 ) } ) → ( 𝑃 ‘ 2 ) ≠ ( 𝑃 ‘ 1 ) ) |
| 90 |
87 89
|
syl |
⊢ ( ( ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ∧ 𝐺 ∈ USGraph ) ∧ 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ) → ( 𝑃 ‘ 2 ) ≠ ( 𝑃 ‘ 1 ) ) |
| 91 |
80 90
|
nelprd |
⊢ ( ( ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ∧ 𝐺 ∈ USGraph ) ∧ 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ) → ¬ ( 𝑃 ‘ 2 ) ∈ { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ) |
| 92 |
44 91
|
eldifd |
⊢ ( ( ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ∧ 𝐺 ∈ USGraph ) ∧ 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ) → ( 𝑃 ‘ 2 ) ∈ ( 𝑉 ∖ { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ) ) |
| 93 |
92
|
ad2antrr |
⊢ ( ( ( ( ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ∧ 𝐺 ∈ USGraph ) ∧ 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ) ∧ 𝑥 = ( 𝑃 ‘ 0 ) ) ∧ 𝑦 = ( 𝑃 ‘ 1 ) ) → ( 𝑃 ‘ 2 ) ∈ ( 𝑉 ∖ { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ) ) |
| 94 |
|
preq12 |
⊢ ( ( 𝑥 = ( 𝑃 ‘ 0 ) ∧ 𝑦 = ( 𝑃 ‘ 1 ) ) → { 𝑥 , 𝑦 } = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ) |
| 95 |
94
|
difeq2d |
⊢ ( ( 𝑥 = ( 𝑃 ‘ 0 ) ∧ 𝑦 = ( 𝑃 ‘ 1 ) ) → ( 𝑉 ∖ { 𝑥 , 𝑦 } ) = ( 𝑉 ∖ { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ) ) |
| 96 |
95
|
eleq2d |
⊢ ( ( 𝑥 = ( 𝑃 ‘ 0 ) ∧ 𝑦 = ( 𝑃 ‘ 1 ) ) → ( ( 𝑃 ‘ 2 ) ∈ ( 𝑉 ∖ { 𝑥 , 𝑦 } ) ↔ ( 𝑃 ‘ 2 ) ∈ ( 𝑉 ∖ { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ) ) ) |
| 97 |
96
|
adantll |
⊢ ( ( ( ( ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ∧ 𝐺 ∈ USGraph ) ∧ 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ) ∧ 𝑥 = ( 𝑃 ‘ 0 ) ) ∧ 𝑦 = ( 𝑃 ‘ 1 ) ) → ( ( 𝑃 ‘ 2 ) ∈ ( 𝑉 ∖ { 𝑥 , 𝑦 } ) ↔ ( 𝑃 ‘ 2 ) ∈ ( 𝑉 ∖ { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ) ) ) |
| 98 |
93 97
|
mpbird |
⊢ ( ( ( ( ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ∧ 𝐺 ∈ USGraph ) ∧ 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ) ∧ 𝑥 = ( 𝑃 ‘ 0 ) ) ∧ 𝑦 = ( 𝑃 ‘ 1 ) ) → ( 𝑃 ‘ 2 ) ∈ ( 𝑉 ∖ { 𝑥 , 𝑦 } ) ) |
| 99 |
|
eqcom |
⊢ ( 𝑥 = ( 𝑃 ‘ 0 ) ↔ ( 𝑃 ‘ 0 ) = 𝑥 ) |
| 100 |
|
eqcom |
⊢ ( 𝑦 = ( 𝑃 ‘ 1 ) ↔ ( 𝑃 ‘ 1 ) = 𝑦 ) |
| 101 |
|
eqcom |
⊢ ( 𝑧 = ( 𝑃 ‘ 2 ) ↔ ( 𝑃 ‘ 2 ) = 𝑧 ) |
| 102 |
99 100 101
|
3anbi123i |
⊢ ( ( 𝑥 = ( 𝑃 ‘ 0 ) ∧ 𝑦 = ( 𝑃 ‘ 1 ) ∧ 𝑧 = ( 𝑃 ‘ 2 ) ) ↔ ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) ) |
| 103 |
102
|
biimpi |
⊢ ( ( 𝑥 = ( 𝑃 ‘ 0 ) ∧ 𝑦 = ( 𝑃 ‘ 1 ) ∧ 𝑧 = ( 𝑃 ‘ 2 ) ) → ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) ) |
| 104 |
103
|
ad4ant123 |
⊢ ( ( ( ( 𝑥 = ( 𝑃 ‘ 0 ) ∧ 𝑦 = ( 𝑃 ‘ 1 ) ) ∧ 𝑧 = ( 𝑃 ‘ 2 ) ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) → ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) ) |
| 105 |
99
|
biimpi |
⊢ ( 𝑥 = ( 𝑃 ‘ 0 ) → ( 𝑃 ‘ 0 ) = 𝑥 ) |
| 106 |
105
|
ad2antrr |
⊢ ( ( ( 𝑥 = ( 𝑃 ‘ 0 ) ∧ 𝑦 = ( 𝑃 ‘ 1 ) ) ∧ 𝑧 = ( 𝑃 ‘ 2 ) ) → ( 𝑃 ‘ 0 ) = 𝑥 ) |
| 107 |
100
|
biimpi |
⊢ ( 𝑦 = ( 𝑃 ‘ 1 ) → ( 𝑃 ‘ 1 ) = 𝑦 ) |
| 108 |
107
|
ad2antlr |
⊢ ( ( ( 𝑥 = ( 𝑃 ‘ 0 ) ∧ 𝑦 = ( 𝑃 ‘ 1 ) ) ∧ 𝑧 = ( 𝑃 ‘ 2 ) ) → ( 𝑃 ‘ 1 ) = 𝑦 ) |
| 109 |
106 108
|
preq12d |
⊢ ( ( ( 𝑥 = ( 𝑃 ‘ 0 ) ∧ 𝑦 = ( 𝑃 ‘ 1 ) ) ∧ 𝑧 = ( 𝑃 ‘ 2 ) ) → { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } = { 𝑥 , 𝑦 } ) |
| 110 |
109
|
eqeq2d |
⊢ ( ( ( 𝑥 = ( 𝑃 ‘ 0 ) ∧ 𝑦 = ( 𝑃 ‘ 1 ) ) ∧ 𝑧 = ( 𝑃 ‘ 2 ) ) → ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ↔ ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } ) ) |
| 111 |
101
|
bilani |
⊢ ( ( ( 𝑥 = ( 𝑃 ‘ 0 ) ∧ 𝑦 = ( 𝑃 ‘ 1 ) ) ∧ 𝑧 = ( 𝑃 ‘ 2 ) ) → ( 𝑃 ‘ 2 ) = 𝑧 ) |
| 112 |
108 111
|
preq12d |
⊢ ( ( ( 𝑥 = ( 𝑃 ‘ 0 ) ∧ 𝑦 = ( 𝑃 ‘ 1 ) ) ∧ 𝑧 = ( 𝑃 ‘ 2 ) ) → { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } = { 𝑦 , 𝑧 } ) |
| 113 |
112
|
eqeq2d |
⊢ ( ( ( 𝑥 = ( 𝑃 ‘ 0 ) ∧ 𝑦 = ( 𝑃 ‘ 1 ) ) ∧ 𝑧 = ( 𝑃 ‘ 2 ) ) → ( ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ↔ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } ) ) |
| 114 |
110 113
|
anbi12d |
⊢ ( ( ( 𝑥 = ( 𝑃 ‘ 0 ) ∧ 𝑦 = ( 𝑃 ‘ 1 ) ) ∧ 𝑧 = ( 𝑃 ‘ 2 ) ) → ( ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ↔ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } ) ) ) |
| 115 |
114
|
biimpa |
⊢ ( ( ( ( 𝑥 = ( 𝑃 ‘ 0 ) ∧ 𝑦 = ( 𝑃 ‘ 1 ) ) ∧ 𝑧 = ( 𝑃 ‘ 2 ) ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) → ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } ) ) |
| 116 |
104 115
|
jca |
⊢ ( ( ( ( 𝑥 = ( 𝑃 ‘ 0 ) ∧ 𝑦 = ( 𝑃 ‘ 1 ) ) ∧ 𝑧 = ( 𝑃 ‘ 2 ) ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) → ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } ) ) ) |
| 117 |
116
|
exp41 |
⊢ ( 𝑥 = ( 𝑃 ‘ 0 ) → ( 𝑦 = ( 𝑃 ‘ 1 ) → ( 𝑧 = ( 𝑃 ‘ 2 ) → ( ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) → ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } ) ) ) ) ) ) |
| 118 |
117
|
adantl |
⊢ ( ( ( ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ∧ 𝐺 ∈ USGraph ) ∧ 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ) ∧ 𝑥 = ( 𝑃 ‘ 0 ) ) → ( 𝑦 = ( 𝑃 ‘ 1 ) → ( 𝑧 = ( 𝑃 ‘ 2 ) → ( ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) → ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } ) ) ) ) ) ) |
| 119 |
118
|
imp31 |
⊢ ( ( ( ( ( ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ∧ 𝐺 ∈ USGraph ) ∧ 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ) ∧ 𝑥 = ( 𝑃 ‘ 0 ) ) ∧ 𝑦 = ( 𝑃 ‘ 1 ) ) ∧ 𝑧 = ( 𝑃 ‘ 2 ) ) → ( ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) → ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } ) ) ) ) |
| 120 |
98 119
|
rspcimedv |
⊢ ( ( ( ( ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ∧ 𝐺 ∈ USGraph ) ∧ 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ) ∧ 𝑥 = ( 𝑃 ‘ 0 ) ) ∧ 𝑦 = ( 𝑃 ‘ 1 ) ) → ( ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) → ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑥 , 𝑦 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } ) ) ) ) |
| 121 |
37 120
|
rspcimedv |
⊢ ( ( ( ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ∧ 𝐺 ∈ USGraph ) ∧ 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ) ∧ 𝑥 = ( 𝑃 ‘ 0 ) ) → ( ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) → ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑥 , 𝑦 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } ) ) ) ) |
| 122 |
10 121
|
rspcimedv |
⊢ ( ( ( ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ∧ 𝐺 ∈ USGraph ) ∧ 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ) → ( ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) → ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑥 , 𝑦 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } ) ) ) ) |
| 123 |
122
|
exp41 |
⊢ ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 → ( ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) → ( 𝐺 ∈ USGraph → ( 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 → ( ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) → ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑥 , 𝑦 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } ) ) ) ) ) ) ) |
| 124 |
123
|
com15 |
⊢ ( ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) → ( ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) → ( 𝐺 ∈ USGraph → ( 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 → ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 → ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑥 , 𝑦 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } ) ) ) ) ) ) ) |
| 125 |
124
|
pm2.43i |
⊢ ( ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) → ( 𝐺 ∈ USGraph → ( 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 → ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 → ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑥 , 𝑦 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } ) ) ) ) ) ) |
| 126 |
125
|
com12 |
⊢ ( 𝐺 ∈ USGraph → ( ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) → ( 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 → ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 → ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑥 , 𝑦 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } ) ) ) ) ) ) |
| 127 |
126
|
adantr |
⊢ ( ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝐹 ) = 2 ) → ( ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) → ( 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 → ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 → ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑥 , 𝑦 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } ) ) ) ) ) ) |
| 128 |
|
oveq2 |
⊢ ( ( ♯ ‘ 𝐹 ) = 2 → ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = ( 0 ..^ 2 ) ) |
| 129 |
128
|
raleqdv |
⊢ ( ( ♯ ‘ 𝐹 ) = 2 → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ↔ ∀ 𝑖 ∈ ( 0 ..^ 2 ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) ) |
| 130 |
|
fzo0to2pr |
⊢ ( 0 ..^ 2 ) = { 0 , 1 } |
| 131 |
130
|
raleqi |
⊢ ( ∀ 𝑖 ∈ ( 0 ..^ 2 ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ↔ ∀ 𝑖 ∈ { 0 , 1 } ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) |
| 132 |
|
2wlklem |
⊢ ( ∀ 𝑖 ∈ { 0 , 1 } ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ↔ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) |
| 133 |
131 132
|
bitri |
⊢ ( ∀ 𝑖 ∈ ( 0 ..^ 2 ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ↔ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) |
| 134 |
129 133
|
bitrdi |
⊢ ( ( ♯ ‘ 𝐹 ) = 2 → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ↔ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ) |
| 135 |
134
|
adantl |
⊢ ( ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝐹 ) = 2 ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ↔ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) ) ) |
| 136 |
|
oveq2 |
⊢ ( ( ♯ ‘ 𝐹 ) = 2 → ( 0 ... ( ♯ ‘ 𝐹 ) ) = ( 0 ... 2 ) ) |
| 137 |
136
|
feq2d |
⊢ ( ( ♯ ‘ 𝐹 ) = 2 → ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ↔ 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ) ) |
| 138 |
137
|
adantl |
⊢ ( ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝐹 ) = 2 ) → ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ↔ 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 ) ) |
| 139 |
|
f1eq2 |
⊢ ( ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = ( 0 ..^ 2 ) → ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐼 ↔ 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ) ) |
| 140 |
128 139
|
syl |
⊢ ( ( ♯ ‘ 𝐹 ) = 2 → ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐼 ↔ 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 ) ) |
| 141 |
140
|
imbi1d |
⊢ ( ( ♯ ‘ 𝐹 ) = 2 → ( ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐼 → ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑥 , 𝑦 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } ) ) ) ↔ ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 → ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑥 , 𝑦 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } ) ) ) ) ) |
| 142 |
141
|
adantl |
⊢ ( ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝐹 ) = 2 ) → ( ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐼 → ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑥 , 𝑦 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } ) ) ) ↔ ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 → ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑥 , 𝑦 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } ) ) ) ) ) |
| 143 |
138 142
|
imbi12d |
⊢ ( ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝐹 ) = 2 ) → ( ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 → ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐼 → ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑥 , 𝑦 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } ) ) ) ) ↔ ( 𝑃 : ( 0 ... 2 ) ⟶ 𝑉 → ( 𝐹 : ( 0 ..^ 2 ) –1-1→ dom 𝐼 → ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑥 , 𝑦 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } ) ) ) ) ) ) |
| 144 |
127 135 143
|
3imtr4d |
⊢ ( ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝐹 ) = 2 ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } → ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 → ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐼 → ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑥 , 𝑦 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } ) ) ) ) ) ) |
| 145 |
144
|
com14 |
⊢ ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐼 → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } → ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 → ( ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝐹 ) = 2 ) → ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑥 , 𝑦 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } ) ) ) ) ) ) |
| 146 |
145
|
com23 |
⊢ ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐼 → ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } → ( ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝐹 ) = 2 ) → ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑥 , 𝑦 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } ) ) ) ) ) ) |
| 147 |
146
|
3imp |
⊢ ( ( 𝐹 : ( 0 ..^ ( ♯ ‘ 𝐹 ) ) –1-1→ dom 𝐼 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ 𝑉 ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑖 ) ) = { ( 𝑃 ‘ 𝑖 ) , ( 𝑃 ‘ ( 𝑖 + 1 ) ) } ) → ( ( 𝐺 ∈ USGraph ∧ ( ♯ ‘ 𝐹 ) = 2 ) → ∃ 𝑥 ∈ 𝑉 ∃ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ∃ 𝑧 ∈ ( 𝑉 ∖ { 𝑥 , 𝑦 } ) ( ( ( 𝑃 ‘ 0 ) = 𝑥 ∧ ( 𝑃 ‘ 1 ) = 𝑦 ∧ ( 𝑃 ‘ 2 ) = 𝑧 ) ∧ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { 𝑥 , 𝑦 } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { 𝑦 , 𝑧 } ) ) ) ) |