Proof of Theorem f1otrgitv
Step | Hyp | Ref
| Expression |
1 | | f1otrkg.2 |
. . 3
⊢ ((𝜑 ∧ (𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ∧ 𝑔 ∈ 𝐵)) → (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹‘𝑔) ∈ ((𝐹‘𝑒)𝐼(𝐹‘𝑓)))) |
2 | 1 | ralrimivvva 3115 |
. 2
⊢ (𝜑 → ∀𝑒 ∈ 𝐵 ∀𝑓 ∈ 𝐵 ∀𝑔 ∈ 𝐵 (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹‘𝑔) ∈ ((𝐹‘𝑒)𝐼(𝐹‘𝑓)))) |
3 | | f1otrgitv.x |
. . 3
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
4 | | f1otrgitv.y |
. . 3
⊢ (𝜑 → 𝑌 ∈ 𝐵) |
5 | | f1otrgitv.z |
. . 3
⊢ (𝜑 → 𝑍 ∈ 𝐵) |
6 | | oveq1 7284 |
. . . . . 6
⊢ (𝑒 = 𝑋 → (𝑒𝐽𝑓) = (𝑋𝐽𝑓)) |
7 | 6 | eleq2d 2824 |
. . . . 5
⊢ (𝑒 = 𝑋 → (𝑔 ∈ (𝑒𝐽𝑓) ↔ 𝑔 ∈ (𝑋𝐽𝑓))) |
8 | | fveq2 6776 |
. . . . . . 7
⊢ (𝑒 = 𝑋 → (𝐹‘𝑒) = (𝐹‘𝑋)) |
9 | 8 | oveq1d 7292 |
. . . . . 6
⊢ (𝑒 = 𝑋 → ((𝐹‘𝑒)𝐼(𝐹‘𝑓)) = ((𝐹‘𝑋)𝐼(𝐹‘𝑓))) |
10 | 9 | eleq2d 2824 |
. . . . 5
⊢ (𝑒 = 𝑋 → ((𝐹‘𝑔) ∈ ((𝐹‘𝑒)𝐼(𝐹‘𝑓)) ↔ (𝐹‘𝑔) ∈ ((𝐹‘𝑋)𝐼(𝐹‘𝑓)))) |
11 | 7, 10 | bibi12d 346 |
. . . 4
⊢ (𝑒 = 𝑋 → ((𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹‘𝑔) ∈ ((𝐹‘𝑒)𝐼(𝐹‘𝑓))) ↔ (𝑔 ∈ (𝑋𝐽𝑓) ↔ (𝐹‘𝑔) ∈ ((𝐹‘𝑋)𝐼(𝐹‘𝑓))))) |
12 | | oveq2 7285 |
. . . . . 6
⊢ (𝑓 = 𝑌 → (𝑋𝐽𝑓) = (𝑋𝐽𝑌)) |
13 | 12 | eleq2d 2824 |
. . . . 5
⊢ (𝑓 = 𝑌 → (𝑔 ∈ (𝑋𝐽𝑓) ↔ 𝑔 ∈ (𝑋𝐽𝑌))) |
14 | | fveq2 6776 |
. . . . . . 7
⊢ (𝑓 = 𝑌 → (𝐹‘𝑓) = (𝐹‘𝑌)) |
15 | 14 | oveq2d 7293 |
. . . . . 6
⊢ (𝑓 = 𝑌 → ((𝐹‘𝑋)𝐼(𝐹‘𝑓)) = ((𝐹‘𝑋)𝐼(𝐹‘𝑌))) |
16 | 15 | eleq2d 2824 |
. . . . 5
⊢ (𝑓 = 𝑌 → ((𝐹‘𝑔) ∈ ((𝐹‘𝑋)𝐼(𝐹‘𝑓)) ↔ (𝐹‘𝑔) ∈ ((𝐹‘𝑋)𝐼(𝐹‘𝑌)))) |
17 | 13, 16 | bibi12d 346 |
. . . 4
⊢ (𝑓 = 𝑌 → ((𝑔 ∈ (𝑋𝐽𝑓) ↔ (𝐹‘𝑔) ∈ ((𝐹‘𝑋)𝐼(𝐹‘𝑓))) ↔ (𝑔 ∈ (𝑋𝐽𝑌) ↔ (𝐹‘𝑔) ∈ ((𝐹‘𝑋)𝐼(𝐹‘𝑌))))) |
18 | | eleq1 2826 |
. . . . 5
⊢ (𝑔 = 𝑍 → (𝑔 ∈ (𝑋𝐽𝑌) ↔ 𝑍 ∈ (𝑋𝐽𝑌))) |
19 | | fveq2 6776 |
. . . . . 6
⊢ (𝑔 = 𝑍 → (𝐹‘𝑔) = (𝐹‘𝑍)) |
20 | 19 | eleq1d 2823 |
. . . . 5
⊢ (𝑔 = 𝑍 → ((𝐹‘𝑔) ∈ ((𝐹‘𝑋)𝐼(𝐹‘𝑌)) ↔ (𝐹‘𝑍) ∈ ((𝐹‘𝑋)𝐼(𝐹‘𝑌)))) |
21 | 18, 20 | bibi12d 346 |
. . . 4
⊢ (𝑔 = 𝑍 → ((𝑔 ∈ (𝑋𝐽𝑌) ↔ (𝐹‘𝑔) ∈ ((𝐹‘𝑋)𝐼(𝐹‘𝑌))) ↔ (𝑍 ∈ (𝑋𝐽𝑌) ↔ (𝐹‘𝑍) ∈ ((𝐹‘𝑋)𝐼(𝐹‘𝑌))))) |
22 | 11, 17, 21 | rspc3v 3574 |
. . 3
⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → (∀𝑒 ∈ 𝐵 ∀𝑓 ∈ 𝐵 ∀𝑔 ∈ 𝐵 (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹‘𝑔) ∈ ((𝐹‘𝑒)𝐼(𝐹‘𝑓))) → (𝑍 ∈ (𝑋𝐽𝑌) ↔ (𝐹‘𝑍) ∈ ((𝐹‘𝑋)𝐼(𝐹‘𝑌))))) |
23 | 3, 4, 5, 22 | syl3anc 1370 |
. 2
⊢ (𝜑 → (∀𝑒 ∈ 𝐵 ∀𝑓 ∈ 𝐵 ∀𝑔 ∈ 𝐵 (𝑔 ∈ (𝑒𝐽𝑓) ↔ (𝐹‘𝑔) ∈ ((𝐹‘𝑒)𝐼(𝐹‘𝑓))) → (𝑍 ∈ (𝑋𝐽𝑌) ↔ (𝐹‘𝑍) ∈ ((𝐹‘𝑋)𝐼(𝐹‘𝑌))))) |
24 | 2, 23 | mpd 15 |
1
⊢ (𝜑 → (𝑍 ∈ (𝑋𝐽𝑌) ↔ (𝐹‘𝑍) ∈ ((𝐹‘𝑋)𝐼(𝐹‘𝑌)))) |