| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eqid 2736 | . . . . 5
⊢
(Base‘𝐾) =
(Base‘𝐾) | 
| 2 |  | lautco.i | . . . . 5
⊢ 𝐼 = (LAut‘𝐾) | 
| 3 | 1, 2 | laut1o 40088 | . . . 4
⊢ ((𝐾 ∈ 𝑉 ∧ 𝐹 ∈ 𝐼) → 𝐹:(Base‘𝐾)–1-1-onto→(Base‘𝐾)) | 
| 4 | 3 | 3adant3 1132 | . . 3
⊢ ((𝐾 ∈ 𝑉 ∧ 𝐹 ∈ 𝐼 ∧ 𝐺 ∈ 𝐼) → 𝐹:(Base‘𝐾)–1-1-onto→(Base‘𝐾)) | 
| 5 | 1, 2 | laut1o 40088 | . . . 4
⊢ ((𝐾 ∈ 𝑉 ∧ 𝐺 ∈ 𝐼) → 𝐺:(Base‘𝐾)–1-1-onto→(Base‘𝐾)) | 
| 6 | 5 | 3adant2 1131 | . . 3
⊢ ((𝐾 ∈ 𝑉 ∧ 𝐹 ∈ 𝐼 ∧ 𝐺 ∈ 𝐼) → 𝐺:(Base‘𝐾)–1-1-onto→(Base‘𝐾)) | 
| 7 |  | f1oco 6870 | . . 3
⊢ ((𝐹:(Base‘𝐾)–1-1-onto→(Base‘𝐾) ∧ 𝐺:(Base‘𝐾)–1-1-onto→(Base‘𝐾)) → (𝐹 ∘ 𝐺):(Base‘𝐾)–1-1-onto→(Base‘𝐾)) | 
| 8 | 4, 6, 7 | syl2anc 584 | . 2
⊢ ((𝐾 ∈ 𝑉 ∧ 𝐹 ∈ 𝐼 ∧ 𝐺 ∈ 𝐼) → (𝐹 ∘ 𝐺):(Base‘𝐾)–1-1-onto→(Base‘𝐾)) | 
| 9 |  | simpl1 1191 | . . . . 5
⊢ (((𝐾 ∈ 𝑉 ∧ 𝐹 ∈ 𝐼 ∧ 𝐺 ∈ 𝐼) ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾))) → 𝐾 ∈ 𝑉) | 
| 10 |  | simpl2 1192 | . . . . 5
⊢ (((𝐾 ∈ 𝑉 ∧ 𝐹 ∈ 𝐼 ∧ 𝐺 ∈ 𝐼) ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾))) → 𝐹 ∈ 𝐼) | 
| 11 |  | simpl3 1193 | . . . . . 6
⊢ (((𝐾 ∈ 𝑉 ∧ 𝐹 ∈ 𝐼 ∧ 𝐺 ∈ 𝐼) ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾))) → 𝐺 ∈ 𝐼) | 
| 12 |  | simprl 770 | . . . . . 6
⊢ (((𝐾 ∈ 𝑉 ∧ 𝐹 ∈ 𝐼 ∧ 𝐺 ∈ 𝐼) ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾))) → 𝑥 ∈ (Base‘𝐾)) | 
| 13 | 1, 2 | lautcl 40090 | . . . . . 6
⊢ (((𝐾 ∈ 𝑉 ∧ 𝐺 ∈ 𝐼) ∧ 𝑥 ∈ (Base‘𝐾)) → (𝐺‘𝑥) ∈ (Base‘𝐾)) | 
| 14 | 9, 11, 12, 13 | syl21anc 837 | . . . . 5
⊢ (((𝐾 ∈ 𝑉 ∧ 𝐹 ∈ 𝐼 ∧ 𝐺 ∈ 𝐼) ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾))) → (𝐺‘𝑥) ∈ (Base‘𝐾)) | 
| 15 |  | simprr 772 | . . . . . 6
⊢ (((𝐾 ∈ 𝑉 ∧ 𝐹 ∈ 𝐼 ∧ 𝐺 ∈ 𝐼) ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾))) → 𝑦 ∈ (Base‘𝐾)) | 
| 16 | 1, 2 | lautcl 40090 | . . . . . 6
⊢ (((𝐾 ∈ 𝑉 ∧ 𝐺 ∈ 𝐼) ∧ 𝑦 ∈ (Base‘𝐾)) → (𝐺‘𝑦) ∈ (Base‘𝐾)) | 
| 17 | 9, 11, 15, 16 | syl21anc 837 | . . . . 5
⊢ (((𝐾 ∈ 𝑉 ∧ 𝐹 ∈ 𝐼 ∧ 𝐺 ∈ 𝐼) ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾))) → (𝐺‘𝑦) ∈ (Base‘𝐾)) | 
| 18 |  | eqid 2736 | . . . . . 6
⊢
(le‘𝐾) =
(le‘𝐾) | 
| 19 | 1, 18, 2 | lautle 40087 | . . . . 5
⊢ (((𝐾 ∈ 𝑉 ∧ 𝐹 ∈ 𝐼) ∧ ((𝐺‘𝑥) ∈ (Base‘𝐾) ∧ (𝐺‘𝑦) ∈ (Base‘𝐾))) → ((𝐺‘𝑥)(le‘𝐾)(𝐺‘𝑦) ↔ (𝐹‘(𝐺‘𝑥))(le‘𝐾)(𝐹‘(𝐺‘𝑦)))) | 
| 20 | 9, 10, 14, 17, 19 | syl22anc 838 | . . . 4
⊢ (((𝐾 ∈ 𝑉 ∧ 𝐹 ∈ 𝐼 ∧ 𝐺 ∈ 𝐼) ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾))) → ((𝐺‘𝑥)(le‘𝐾)(𝐺‘𝑦) ↔ (𝐹‘(𝐺‘𝑥))(le‘𝐾)(𝐹‘(𝐺‘𝑦)))) | 
| 21 | 1, 18, 2 | lautle 40087 | . . . . 5
⊢ (((𝐾 ∈ 𝑉 ∧ 𝐺 ∈ 𝐼) ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾))) → (𝑥(le‘𝐾)𝑦 ↔ (𝐺‘𝑥)(le‘𝐾)(𝐺‘𝑦))) | 
| 22 | 21 | 3adantl2 1167 | . . . 4
⊢ (((𝐾 ∈ 𝑉 ∧ 𝐹 ∈ 𝐼 ∧ 𝐺 ∈ 𝐼) ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾))) → (𝑥(le‘𝐾)𝑦 ↔ (𝐺‘𝑥)(le‘𝐾)(𝐺‘𝑦))) | 
| 23 |  | f1of 6847 | . . . . . . 7
⊢ (𝐺:(Base‘𝐾)–1-1-onto→(Base‘𝐾) → 𝐺:(Base‘𝐾)⟶(Base‘𝐾)) | 
| 24 | 6, 23 | syl 17 | . . . . . 6
⊢ ((𝐾 ∈ 𝑉 ∧ 𝐹 ∈ 𝐼 ∧ 𝐺 ∈ 𝐼) → 𝐺:(Base‘𝐾)⟶(Base‘𝐾)) | 
| 25 |  | simpl 482 | . . . . . 6
⊢ ((𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) → 𝑥 ∈ (Base‘𝐾)) | 
| 26 |  | fvco3 7007 | . . . . . 6
⊢ ((𝐺:(Base‘𝐾)⟶(Base‘𝐾) ∧ 𝑥 ∈ (Base‘𝐾)) → ((𝐹 ∘ 𝐺)‘𝑥) = (𝐹‘(𝐺‘𝑥))) | 
| 27 | 24, 25, 26 | syl2an 596 | . . . . 5
⊢ (((𝐾 ∈ 𝑉 ∧ 𝐹 ∈ 𝐼 ∧ 𝐺 ∈ 𝐼) ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾))) → ((𝐹 ∘ 𝐺)‘𝑥) = (𝐹‘(𝐺‘𝑥))) | 
| 28 |  | simpr 484 | . . . . . 6
⊢ ((𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) → 𝑦 ∈ (Base‘𝐾)) | 
| 29 |  | fvco3 7007 | . . . . . 6
⊢ ((𝐺:(Base‘𝐾)⟶(Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾)) → ((𝐹 ∘ 𝐺)‘𝑦) = (𝐹‘(𝐺‘𝑦))) | 
| 30 | 24, 28, 29 | syl2an 596 | . . . . 5
⊢ (((𝐾 ∈ 𝑉 ∧ 𝐹 ∈ 𝐼 ∧ 𝐺 ∈ 𝐼) ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾))) → ((𝐹 ∘ 𝐺)‘𝑦) = (𝐹‘(𝐺‘𝑦))) | 
| 31 | 27, 30 | breq12d 5155 | . . . 4
⊢ (((𝐾 ∈ 𝑉 ∧ 𝐹 ∈ 𝐼 ∧ 𝐺 ∈ 𝐼) ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾))) → (((𝐹 ∘ 𝐺)‘𝑥)(le‘𝐾)((𝐹 ∘ 𝐺)‘𝑦) ↔ (𝐹‘(𝐺‘𝑥))(le‘𝐾)(𝐹‘(𝐺‘𝑦)))) | 
| 32 | 20, 22, 31 | 3bitr4d 311 | . . 3
⊢ (((𝐾 ∈ 𝑉 ∧ 𝐹 ∈ 𝐼 ∧ 𝐺 ∈ 𝐼) ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾))) → (𝑥(le‘𝐾)𝑦 ↔ ((𝐹 ∘ 𝐺)‘𝑥)(le‘𝐾)((𝐹 ∘ 𝐺)‘𝑦))) | 
| 33 | 32 | ralrimivva 3201 | . 2
⊢ ((𝐾 ∈ 𝑉 ∧ 𝐹 ∈ 𝐼 ∧ 𝐺 ∈ 𝐼) → ∀𝑥 ∈ (Base‘𝐾)∀𝑦 ∈ (Base‘𝐾)(𝑥(le‘𝐾)𝑦 ↔ ((𝐹 ∘ 𝐺)‘𝑥)(le‘𝐾)((𝐹 ∘ 𝐺)‘𝑦))) | 
| 34 | 1, 18, 2 | islaut 40086 | . . 3
⊢ (𝐾 ∈ 𝑉 → ((𝐹 ∘ 𝐺) ∈ 𝐼 ↔ ((𝐹 ∘ 𝐺):(Base‘𝐾)–1-1-onto→(Base‘𝐾) ∧ ∀𝑥 ∈ (Base‘𝐾)∀𝑦 ∈ (Base‘𝐾)(𝑥(le‘𝐾)𝑦 ↔ ((𝐹 ∘ 𝐺)‘𝑥)(le‘𝐾)((𝐹 ∘ 𝐺)‘𝑦))))) | 
| 35 | 34 | 3ad2ant1 1133 | . 2
⊢ ((𝐾 ∈ 𝑉 ∧ 𝐹 ∈ 𝐼 ∧ 𝐺 ∈ 𝐼) → ((𝐹 ∘ 𝐺) ∈ 𝐼 ↔ ((𝐹 ∘ 𝐺):(Base‘𝐾)–1-1-onto→(Base‘𝐾) ∧ ∀𝑥 ∈ (Base‘𝐾)∀𝑦 ∈ (Base‘𝐾)(𝑥(le‘𝐾)𝑦 ↔ ((𝐹 ∘ 𝐺)‘𝑥)(le‘𝐾)((𝐹 ∘ 𝐺)‘𝑦))))) | 
| 36 | 8, 33, 35 | mpbir2and 713 | 1
⊢ ((𝐾 ∈ 𝑉 ∧ 𝐹 ∈ 𝐼 ∧ 𝐺 ∈ 𝐼) → (𝐹 ∘ 𝐺) ∈ 𝐼) |