![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > enctlem | GIF version |
Description: Lemma for enct 12452. One direction of the biconditional. (Contributed by Jim Kingdon, 23-Dec-2023.) |
Ref | Expression |
---|---|
enctlem | ⊢ (𝐴 ≈ 𝐵 → (∃𝑓 𝑓:ω–onto→(𝐴 ⊔ 1o) → ∃𝑔 𝑔:ω–onto→(𝐵 ⊔ 1o))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 1oex 6443 | . . . . 5 ⊢ 1o ∈ V | |
2 | 1 | enref 6783 | . . . 4 ⊢ 1o ≈ 1o |
3 | djuen 7228 | . . . 4 ⊢ ((𝐴 ≈ 𝐵 ∧ 1o ≈ 1o) → (𝐴 ⊔ 1o) ≈ (𝐵 ⊔ 1o)) | |
4 | 2, 3 | mpan2 425 | . . 3 ⊢ (𝐴 ≈ 𝐵 → (𝐴 ⊔ 1o) ≈ (𝐵 ⊔ 1o)) |
5 | bren 6765 | . . 3 ⊢ ((𝐴 ⊔ 1o) ≈ (𝐵 ⊔ 1o) ↔ ∃ℎ ℎ:(𝐴 ⊔ 1o)–1-1-onto→(𝐵 ⊔ 1o)) | |
6 | 4, 5 | sylib 122 | . 2 ⊢ (𝐴 ≈ 𝐵 → ∃ℎ ℎ:(𝐴 ⊔ 1o)–1-1-onto→(𝐵 ⊔ 1o)) |
7 | f1ofo 5483 | . . . . . 6 ⊢ (ℎ:(𝐴 ⊔ 1o)–1-1-onto→(𝐵 ⊔ 1o) → ℎ:(𝐴 ⊔ 1o)–onto→(𝐵 ⊔ 1o)) | |
8 | 7 | ad2antlr 489 | . . . . 5 ⊢ (((𝐴 ≈ 𝐵 ∧ ℎ:(𝐴 ⊔ 1o)–1-1-onto→(𝐵 ⊔ 1o)) ∧ 𝑓:ω–onto→(𝐴 ⊔ 1o)) → ℎ:(𝐴 ⊔ 1o)–onto→(𝐵 ⊔ 1o)) |
9 | foco 5463 | . . . . . 6 ⊢ ((ℎ:(𝐴 ⊔ 1o)–onto→(𝐵 ⊔ 1o) ∧ 𝑓:ω–onto→(𝐴 ⊔ 1o)) → (ℎ ∘ 𝑓):ω–onto→(𝐵 ⊔ 1o)) | |
10 | vex 2755 | . . . . . . . 8 ⊢ ℎ ∈ V | |
11 | vex 2755 | . . . . . . . 8 ⊢ 𝑓 ∈ V | |
12 | 10, 11 | coex 5189 | . . . . . . 7 ⊢ (ℎ ∘ 𝑓) ∈ V |
13 | foeq1 5449 | . . . . . . 7 ⊢ (𝑔 = (ℎ ∘ 𝑓) → (𝑔:ω–onto→(𝐵 ⊔ 1o) ↔ (ℎ ∘ 𝑓):ω–onto→(𝐵 ⊔ 1o))) | |
14 | 12, 13 | spcev 2847 | . . . . . 6 ⊢ ((ℎ ∘ 𝑓):ω–onto→(𝐵 ⊔ 1o) → ∃𝑔 𝑔:ω–onto→(𝐵 ⊔ 1o)) |
15 | 9, 14 | syl 14 | . . . . 5 ⊢ ((ℎ:(𝐴 ⊔ 1o)–onto→(𝐵 ⊔ 1o) ∧ 𝑓:ω–onto→(𝐴 ⊔ 1o)) → ∃𝑔 𝑔:ω–onto→(𝐵 ⊔ 1o)) |
16 | 8, 15 | sylancom 420 | . . . 4 ⊢ (((𝐴 ≈ 𝐵 ∧ ℎ:(𝐴 ⊔ 1o)–1-1-onto→(𝐵 ⊔ 1o)) ∧ 𝑓:ω–onto→(𝐴 ⊔ 1o)) → ∃𝑔 𝑔:ω–onto→(𝐵 ⊔ 1o)) |
17 | 16 | ex 115 | . . 3 ⊢ ((𝐴 ≈ 𝐵 ∧ ℎ:(𝐴 ⊔ 1o)–1-1-onto→(𝐵 ⊔ 1o)) → (𝑓:ω–onto→(𝐴 ⊔ 1o) → ∃𝑔 𝑔:ω–onto→(𝐵 ⊔ 1o))) |
18 | 17 | exlimdv 1830 | . 2 ⊢ ((𝐴 ≈ 𝐵 ∧ ℎ:(𝐴 ⊔ 1o)–1-1-onto→(𝐵 ⊔ 1o)) → (∃𝑓 𝑓:ω–onto→(𝐴 ⊔ 1o) → ∃𝑔 𝑔:ω–onto→(𝐵 ⊔ 1o))) |
19 | 6, 18 | exlimddv 1910 | 1 ⊢ (𝐴 ≈ 𝐵 → (∃𝑓 𝑓:ω–onto→(𝐴 ⊔ 1o) → ∃𝑔 𝑔:ω–onto→(𝐵 ⊔ 1o))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 ∃wex 1503 class class class wbr 4018 ωcom 4604 ∘ ccom 4645 –onto→wfo 5229 –1-1-onto→wf1o 5230 1oc1o 6428 ≈ cen 6756 ⊔ cdju 7054 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 615 ax-in2 616 ax-io 710 ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-13 2162 ax-14 2163 ax-ext 2171 ax-coll 4133 ax-sep 4136 ax-nul 4144 ax-pow 4189 ax-pr 4224 ax-un 4448 |
This theorem depends on definitions: df-bi 117 df-3an 982 df-tru 1367 df-fal 1370 df-nf 1472 df-sb 1774 df-eu 2041 df-mo 2042 df-clab 2176 df-cleq 2182 df-clel 2185 df-nfc 2321 df-ne 2361 df-ral 2473 df-rex 2474 df-reu 2475 df-rab 2477 df-v 2754 df-sbc 2978 df-csb 3073 df-dif 3146 df-un 3148 df-in 3150 df-ss 3157 df-nul 3438 df-pw 3592 df-sn 3613 df-pr 3614 df-op 3616 df-uni 3825 df-iun 3903 df-br 4019 df-opab 4080 df-mpt 4081 df-tr 4117 df-id 4308 df-iord 4381 df-on 4383 df-suc 4386 df-xp 4647 df-rel 4648 df-cnv 4649 df-co 4650 df-dm 4651 df-rn 4652 df-res 4653 df-ima 4654 df-iota 5193 df-fun 5233 df-fn 5234 df-f 5235 df-f1 5236 df-fo 5237 df-f1o 5238 df-fv 5239 df-1st 6159 df-2nd 6160 df-1o 6435 df-er 6553 df-en 6759 df-dju 7055 df-inl 7064 df-inr 7065 |
This theorem is referenced by: enct 12452 |
Copyright terms: Public domain | W3C validator |