Step | Hyp | Ref
| Expression |
1 | | tgjustc2.p |
. . . . 5
⊢ 𝑃 = (Base‘𝐺) |
2 | | fvex 6459 |
. . . . 5
⊢
(Base‘𝐺)
∈ V |
3 | 1, 2 | eqeltri 2855 |
. . . 4
⊢ 𝑃 ∈ V |
4 | 3, 3 | xpex 7240 |
. . 3
⊢ (𝑃 × 𝑃) ∈ V |
5 | | tgjustc2.d |
. . 3
⊢ 𝑅 Er (𝑃 × 𝑃) |
6 | | tgjustr 25825 |
. . 3
⊢ (((𝑃 × 𝑃) ∈ V ∧ 𝑅 Er (𝑃 × 𝑃)) → ∃𝑑(𝑑 Fn (𝑃 × 𝑃) ∧ ∀𝑢 ∈ (𝑃 × 𝑃)∀𝑣 ∈ (𝑃 × 𝑃)(𝑢𝑅𝑣 ↔ (𝑑‘𝑢) = (𝑑‘𝑣)))) |
7 | 4, 5, 6 | mp2an 682 |
. 2
⊢
∃𝑑(𝑑 Fn (𝑃 × 𝑃) ∧ ∀𝑢 ∈ (𝑃 × 𝑃)∀𝑣 ∈ (𝑃 × 𝑃)(𝑢𝑅𝑣 ↔ (𝑑‘𝑢) = (𝑑‘𝑣))) |
8 | | simplrl 767 |
. . . . . . 7
⊢
(((∀𝑢 ∈
(𝑃 × 𝑃)∀𝑣 ∈ (𝑃 × 𝑃)(𝑢𝑅𝑣 ↔ (𝑑‘𝑢) = (𝑑‘𝑣)) ∧ (𝑤 ∈ 𝑃 ∧ 𝑥 ∈ 𝑃)) ∧ (𝑦 ∈ 𝑃 ∧ 𝑧 ∈ 𝑃)) → 𝑤 ∈ 𝑃) |
9 | | simplrr 768 |
. . . . . . 7
⊢
(((∀𝑢 ∈
(𝑃 × 𝑃)∀𝑣 ∈ (𝑃 × 𝑃)(𝑢𝑅𝑣 ↔ (𝑑‘𝑢) = (𝑑‘𝑣)) ∧ (𝑤 ∈ 𝑃 ∧ 𝑥 ∈ 𝑃)) ∧ (𝑦 ∈ 𝑃 ∧ 𝑧 ∈ 𝑃)) → 𝑥 ∈ 𝑃) |
10 | 8, 9 | opelxpd 5393 |
. . . . . 6
⊢
(((∀𝑢 ∈
(𝑃 × 𝑃)∀𝑣 ∈ (𝑃 × 𝑃)(𝑢𝑅𝑣 ↔ (𝑑‘𝑢) = (𝑑‘𝑣)) ∧ (𝑤 ∈ 𝑃 ∧ 𝑥 ∈ 𝑃)) ∧ (𝑦 ∈ 𝑃 ∧ 𝑧 ∈ 𝑃)) → 〈𝑤, 𝑥〉 ∈ (𝑃 × 𝑃)) |
11 | | simprl 761 |
. . . . . . 7
⊢
(((∀𝑢 ∈
(𝑃 × 𝑃)∀𝑣 ∈ (𝑃 × 𝑃)(𝑢𝑅𝑣 ↔ (𝑑‘𝑢) = (𝑑‘𝑣)) ∧ (𝑤 ∈ 𝑃 ∧ 𝑥 ∈ 𝑃)) ∧ (𝑦 ∈ 𝑃 ∧ 𝑧 ∈ 𝑃)) → 𝑦 ∈ 𝑃) |
12 | | simprr 763 |
. . . . . . 7
⊢
(((∀𝑢 ∈
(𝑃 × 𝑃)∀𝑣 ∈ (𝑃 × 𝑃)(𝑢𝑅𝑣 ↔ (𝑑‘𝑢) = (𝑑‘𝑣)) ∧ (𝑤 ∈ 𝑃 ∧ 𝑥 ∈ 𝑃)) ∧ (𝑦 ∈ 𝑃 ∧ 𝑧 ∈ 𝑃)) → 𝑧 ∈ 𝑃) |
13 | 11, 12 | opelxpd 5393 |
. . . . . 6
⊢
(((∀𝑢 ∈
(𝑃 × 𝑃)∀𝑣 ∈ (𝑃 × 𝑃)(𝑢𝑅𝑣 ↔ (𝑑‘𝑢) = (𝑑‘𝑣)) ∧ (𝑤 ∈ 𝑃 ∧ 𝑥 ∈ 𝑃)) ∧ (𝑦 ∈ 𝑃 ∧ 𝑧 ∈ 𝑃)) → 〈𝑦, 𝑧〉 ∈ (𝑃 × 𝑃)) |
14 | | simpll 757 |
. . . . . 6
⊢
(((∀𝑢 ∈
(𝑃 × 𝑃)∀𝑣 ∈ (𝑃 × 𝑃)(𝑢𝑅𝑣 ↔ (𝑑‘𝑢) = (𝑑‘𝑣)) ∧ (𝑤 ∈ 𝑃 ∧ 𝑥 ∈ 𝑃)) ∧ (𝑦 ∈ 𝑃 ∧ 𝑧 ∈ 𝑃)) → ∀𝑢 ∈ (𝑃 × 𝑃)∀𝑣 ∈ (𝑃 × 𝑃)(𝑢𝑅𝑣 ↔ (𝑑‘𝑢) = (𝑑‘𝑣))) |
15 | | breq1 4889 |
. . . . . . . 8
⊢ (𝑢 = 〈𝑤, 𝑥〉 → (𝑢𝑅𝑣 ↔ 〈𝑤, 𝑥〉𝑅𝑣)) |
16 | | fveq2 6446 |
. . . . . . . . . 10
⊢ (𝑢 = 〈𝑤, 𝑥〉 → (𝑑‘𝑢) = (𝑑‘〈𝑤, 𝑥〉)) |
17 | | df-ov 6925 |
. . . . . . . . . 10
⊢ (𝑤𝑑𝑥) = (𝑑‘〈𝑤, 𝑥〉) |
18 | 16, 17 | syl6eqr 2832 |
. . . . . . . . 9
⊢ (𝑢 = 〈𝑤, 𝑥〉 → (𝑑‘𝑢) = (𝑤𝑑𝑥)) |
19 | 18 | eqeq1d 2780 |
. . . . . . . 8
⊢ (𝑢 = 〈𝑤, 𝑥〉 → ((𝑑‘𝑢) = (𝑑‘𝑣) ↔ (𝑤𝑑𝑥) = (𝑑‘𝑣))) |
20 | 15, 19 | bibi12d 337 |
. . . . . . 7
⊢ (𝑢 = 〈𝑤, 𝑥〉 → ((𝑢𝑅𝑣 ↔ (𝑑‘𝑢) = (𝑑‘𝑣)) ↔ (〈𝑤, 𝑥〉𝑅𝑣 ↔ (𝑤𝑑𝑥) = (𝑑‘𝑣)))) |
21 | | breq2 4890 |
. . . . . . . 8
⊢ (𝑣 = 〈𝑦, 𝑧〉 → (〈𝑤, 𝑥〉𝑅𝑣 ↔ 〈𝑤, 𝑥〉𝑅〈𝑦, 𝑧〉)) |
22 | | fveq2 6446 |
. . . . . . . . . 10
⊢ (𝑣 = 〈𝑦, 𝑧〉 → (𝑑‘𝑣) = (𝑑‘〈𝑦, 𝑧〉)) |
23 | | df-ov 6925 |
. . . . . . . . . 10
⊢ (𝑦𝑑𝑧) = (𝑑‘〈𝑦, 𝑧〉) |
24 | 22, 23 | syl6eqr 2832 |
. . . . . . . . 9
⊢ (𝑣 = 〈𝑦, 𝑧〉 → (𝑑‘𝑣) = (𝑦𝑑𝑧)) |
25 | 24 | eqeq2d 2788 |
. . . . . . . 8
⊢ (𝑣 = 〈𝑦, 𝑧〉 → ((𝑤𝑑𝑥) = (𝑑‘𝑣) ↔ (𝑤𝑑𝑥) = (𝑦𝑑𝑧))) |
26 | 21, 25 | bibi12d 337 |
. . . . . . 7
⊢ (𝑣 = 〈𝑦, 𝑧〉 → ((〈𝑤, 𝑥〉𝑅𝑣 ↔ (𝑤𝑑𝑥) = (𝑑‘𝑣)) ↔ (〈𝑤, 𝑥〉𝑅〈𝑦, 𝑧〉 ↔ (𝑤𝑑𝑥) = (𝑦𝑑𝑧)))) |
27 | 20, 26 | rspc2va 3525 |
. . . . . 6
⊢
(((〈𝑤, 𝑥〉 ∈ (𝑃 × 𝑃) ∧ 〈𝑦, 𝑧〉 ∈ (𝑃 × 𝑃)) ∧ ∀𝑢 ∈ (𝑃 × 𝑃)∀𝑣 ∈ (𝑃 × 𝑃)(𝑢𝑅𝑣 ↔ (𝑑‘𝑢) = (𝑑‘𝑣))) → (〈𝑤, 𝑥〉𝑅〈𝑦, 𝑧〉 ↔ (𝑤𝑑𝑥) = (𝑦𝑑𝑧))) |
28 | 10, 13, 14, 27 | syl21anc 828 |
. . . . 5
⊢
(((∀𝑢 ∈
(𝑃 × 𝑃)∀𝑣 ∈ (𝑃 × 𝑃)(𝑢𝑅𝑣 ↔ (𝑑‘𝑢) = (𝑑‘𝑣)) ∧ (𝑤 ∈ 𝑃 ∧ 𝑥 ∈ 𝑃)) ∧ (𝑦 ∈ 𝑃 ∧ 𝑧 ∈ 𝑃)) → (〈𝑤, 𝑥〉𝑅〈𝑦, 𝑧〉 ↔ (𝑤𝑑𝑥) = (𝑦𝑑𝑧))) |
29 | 28 | ralrimivva 3153 |
. . . 4
⊢
((∀𝑢 ∈
(𝑃 × 𝑃)∀𝑣 ∈ (𝑃 × 𝑃)(𝑢𝑅𝑣 ↔ (𝑑‘𝑢) = (𝑑‘𝑣)) ∧ (𝑤 ∈ 𝑃 ∧ 𝑥 ∈ 𝑃)) → ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 (〈𝑤, 𝑥〉𝑅〈𝑦, 𝑧〉 ↔ (𝑤𝑑𝑥) = (𝑦𝑑𝑧))) |
30 | 29 | ralrimivva 3153 |
. . 3
⊢
(∀𝑢 ∈
(𝑃 × 𝑃)∀𝑣 ∈ (𝑃 × 𝑃)(𝑢𝑅𝑣 ↔ (𝑑‘𝑢) = (𝑑‘𝑣)) → ∀𝑤 ∈ 𝑃 ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 (〈𝑤, 𝑥〉𝑅〈𝑦, 𝑧〉 ↔ (𝑤𝑑𝑥) = (𝑦𝑑𝑧))) |
31 | 30 | anim2i 610 |
. 2
⊢ ((𝑑 Fn (𝑃 × 𝑃) ∧ ∀𝑢 ∈ (𝑃 × 𝑃)∀𝑣 ∈ (𝑃 × 𝑃)(𝑢𝑅𝑣 ↔ (𝑑‘𝑢) = (𝑑‘𝑣))) → (𝑑 Fn (𝑃 × 𝑃) ∧ ∀𝑤 ∈ 𝑃 ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 (〈𝑤, 𝑥〉𝑅〈𝑦, 𝑧〉 ↔ (𝑤𝑑𝑥) = (𝑦𝑑𝑧)))) |
32 | 7, 31 | eximii 1880 |
1
⊢
∃𝑑(𝑑 Fn (𝑃 × 𝑃) ∧ ∀𝑤 ∈ 𝑃 ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 ∀𝑧 ∈ 𝑃 (〈𝑤, 𝑥〉𝑅〈𝑦, 𝑧〉 ↔ (𝑤𝑑𝑥) = (𝑦𝑑𝑧))) |