Proof of Theorem oemapvali
Step | Hyp | Ref
| Expression |
1 | | oemapvali.r |
. . 3
⊢ (𝜑 → 𝐹𝑇𝐺) |
2 | | cantnfs.s |
. . . 4
⊢ 𝑆 = dom (𝐴 CNF 𝐵) |
3 | | cantnfs.a |
. . . 4
⊢ (𝜑 → 𝐴 ∈ On) |
4 | | cantnfs.b |
. . . 4
⊢ (𝜑 → 𝐵 ∈ On) |
5 | | oemapval.t |
. . . 4
⊢ 𝑇 = {〈𝑥, 𝑦〉 ∣ ∃𝑧 ∈ 𝐵 ((𝑥‘𝑧) ∈ (𝑦‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝑥‘𝑤) = (𝑦‘𝑤)))} |
6 | | oemapval.f |
. . . 4
⊢ (𝜑 → 𝐹 ∈ 𝑆) |
7 | | oemapval.g |
. . . 4
⊢ (𝜑 → 𝐺 ∈ 𝑆) |
8 | 2, 3, 4, 5, 6, 7 | oemapval 9212 |
. . 3
⊢ (𝜑 → (𝐹𝑇𝐺 ↔ ∃𝑧 ∈ 𝐵 ((𝐹‘𝑧) ∈ (𝐺‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤))))) |
9 | 1, 8 | mpbid 235 |
. 2
⊢ (𝜑 → ∃𝑧 ∈ 𝐵 ((𝐹‘𝑧) ∈ (𝐺‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤)))) |
10 | | ssrab2 3967 |
. . . 4
⊢ {𝑐 ∈ 𝐵 ∣ (𝐹‘𝑐) ∈ (𝐺‘𝑐)} ⊆ 𝐵 |
11 | | oemapvali.x |
. . . . 5
⊢ 𝑋 = ∪
{𝑐 ∈ 𝐵 ∣ (𝐹‘𝑐) ∈ (𝐺‘𝑐)} |
12 | 4 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ ((𝐹‘𝑧) ∈ (𝐺‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤))))) → 𝐵 ∈ On) |
13 | | onss 7518 |
. . . . . . . 8
⊢ (𝐵 ∈ On → 𝐵 ⊆ On) |
14 | 12, 13 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ ((𝐹‘𝑧) ∈ (𝐺‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤))))) → 𝐵 ⊆ On) |
15 | 10, 14 | sstrid 3886 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ ((𝐹‘𝑧) ∈ (𝐺‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤))))) → {𝑐 ∈ 𝐵 ∣ (𝐹‘𝑐) ∈ (𝐺‘𝑐)} ⊆ On) |
16 | 2, 3, 4 | cantnfs 9195 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐺 ∈ 𝑆 ↔ (𝐺:𝐵⟶𝐴 ∧ 𝐺 finSupp ∅))) |
17 | 7, 16 | mpbid 235 |
. . . . . . . . 9
⊢ (𝜑 → (𝐺:𝐵⟶𝐴 ∧ 𝐺 finSupp ∅)) |
18 | 17 | simprd 499 |
. . . . . . . 8
⊢ (𝜑 → 𝐺 finSupp ∅) |
19 | 18 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ ((𝐹‘𝑧) ∈ (𝐺‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤))))) → 𝐺 finSupp ∅) |
20 | 4 | 3ad2ant1 1134 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐵 ∧ (𝐹‘𝑐) ∈ (𝐺‘𝑐)) → 𝐵 ∈ On) |
21 | | simp2 1138 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐵 ∧ (𝐹‘𝑐) ∈ (𝐺‘𝑐)) → 𝑐 ∈ 𝐵) |
22 | 17 | simpld 498 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐺:𝐵⟶𝐴) |
23 | 22 | ffnd 6499 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐺 Fn 𝐵) |
24 | 23 | 3ad2ant1 1134 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐵 ∧ (𝐹‘𝑐) ∈ (𝐺‘𝑐)) → 𝐺 Fn 𝐵) |
25 | | ne0i 4221 |
. . . . . . . . . . 11
⊢ ((𝐹‘𝑐) ∈ (𝐺‘𝑐) → (𝐺‘𝑐) ≠ ∅) |
26 | 25 | 3ad2ant3 1136 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐵 ∧ (𝐹‘𝑐) ∈ (𝐺‘𝑐)) → (𝐺‘𝑐) ≠ ∅) |
27 | | fvn0elsupp 7868 |
. . . . . . . . . 10
⊢ (((𝐵 ∈ On ∧ 𝑐 ∈ 𝐵) ∧ (𝐺 Fn 𝐵 ∧ (𝐺‘𝑐) ≠ ∅)) → 𝑐 ∈ (𝐺 supp ∅)) |
28 | 20, 21, 24, 26, 27 | syl22anc 838 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐵 ∧ (𝐹‘𝑐) ∈ (𝐺‘𝑐)) → 𝑐 ∈ (𝐺 supp ∅)) |
29 | 28 | rabssdv 3962 |
. . . . . . . 8
⊢ (𝜑 → {𝑐 ∈ 𝐵 ∣ (𝐹‘𝑐) ∈ (𝐺‘𝑐)} ⊆ (𝐺 supp ∅)) |
30 | 29 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ ((𝐹‘𝑧) ∈ (𝐺‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤))))) → {𝑐 ∈ 𝐵 ∣ (𝐹‘𝑐) ∈ (𝐺‘𝑐)} ⊆ (𝐺 supp ∅)) |
31 | | fsuppimp 8905 |
. . . . . . . 8
⊢ (𝐺 finSupp ∅ → (Fun
𝐺 ∧ (𝐺 supp ∅) ∈ Fin)) |
32 | | ssfi 8765 |
. . . . . . . . 9
⊢ (((𝐺 supp ∅) ∈ Fin ∧
{𝑐 ∈ 𝐵 ∣ (𝐹‘𝑐) ∈ (𝐺‘𝑐)} ⊆ (𝐺 supp ∅)) → {𝑐 ∈ 𝐵 ∣ (𝐹‘𝑐) ∈ (𝐺‘𝑐)} ∈ Fin) |
33 | 32 | ex 416 |
. . . . . . . 8
⊢ ((𝐺 supp ∅) ∈ Fin →
({𝑐 ∈ 𝐵 ∣ (𝐹‘𝑐) ∈ (𝐺‘𝑐)} ⊆ (𝐺 supp ∅) → {𝑐 ∈ 𝐵 ∣ (𝐹‘𝑐) ∈ (𝐺‘𝑐)} ∈ Fin)) |
34 | 31, 33 | simpl2im 507 |
. . . . . . 7
⊢ (𝐺 finSupp ∅ → ({𝑐 ∈ 𝐵 ∣ (𝐹‘𝑐) ∈ (𝐺‘𝑐)} ⊆ (𝐺 supp ∅) → {𝑐 ∈ 𝐵 ∣ (𝐹‘𝑐) ∈ (𝐺‘𝑐)} ∈ Fin)) |
35 | 19, 30, 34 | sylc 65 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ ((𝐹‘𝑧) ∈ (𝐺‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤))))) → {𝑐 ∈ 𝐵 ∣ (𝐹‘𝑐) ∈ (𝐺‘𝑐)} ∈ Fin) |
36 | | fveq2 6668 |
. . . . . . . . 9
⊢ (𝑐 = 𝑧 → (𝐹‘𝑐) = (𝐹‘𝑧)) |
37 | | fveq2 6668 |
. . . . . . . . 9
⊢ (𝑐 = 𝑧 → (𝐺‘𝑐) = (𝐺‘𝑧)) |
38 | 36, 37 | eleq12d 2827 |
. . . . . . . 8
⊢ (𝑐 = 𝑧 → ((𝐹‘𝑐) ∈ (𝐺‘𝑐) ↔ (𝐹‘𝑧) ∈ (𝐺‘𝑧))) |
39 | | simprl 771 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ ((𝐹‘𝑧) ∈ (𝐺‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤))))) → 𝑧 ∈ 𝐵) |
40 | | simprrl 781 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ ((𝐹‘𝑧) ∈ (𝐺‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤))))) → (𝐹‘𝑧) ∈ (𝐺‘𝑧)) |
41 | 38, 39, 40 | elrabd 3587 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ ((𝐹‘𝑧) ∈ (𝐺‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤))))) → 𝑧 ∈ {𝑐 ∈ 𝐵 ∣ (𝐹‘𝑐) ∈ (𝐺‘𝑐)}) |
42 | 41 | ne0d 4222 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ ((𝐹‘𝑧) ∈ (𝐺‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤))))) → {𝑐 ∈ 𝐵 ∣ (𝐹‘𝑐) ∈ (𝐺‘𝑐)} ≠ ∅) |
43 | | ordunifi 8835 |
. . . . . 6
⊢ (({𝑐 ∈ 𝐵 ∣ (𝐹‘𝑐) ∈ (𝐺‘𝑐)} ⊆ On ∧ {𝑐 ∈ 𝐵 ∣ (𝐹‘𝑐) ∈ (𝐺‘𝑐)} ∈ Fin ∧ {𝑐 ∈ 𝐵 ∣ (𝐹‘𝑐) ∈ (𝐺‘𝑐)} ≠ ∅) → ∪ {𝑐
∈ 𝐵 ∣ (𝐹‘𝑐) ∈ (𝐺‘𝑐)} ∈ {𝑐 ∈ 𝐵 ∣ (𝐹‘𝑐) ∈ (𝐺‘𝑐)}) |
44 | 15, 35, 42, 43 | syl3anc 1372 |
. . . . 5
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ ((𝐹‘𝑧) ∈ (𝐺‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤))))) → ∪
{𝑐 ∈ 𝐵 ∣ (𝐹‘𝑐) ∈ (𝐺‘𝑐)} ∈ {𝑐 ∈ 𝐵 ∣ (𝐹‘𝑐) ∈ (𝐺‘𝑐)}) |
45 | 11, 44 | eqeltrid 2837 |
. . . 4
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ ((𝐹‘𝑧) ∈ (𝐺‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤))))) → 𝑋 ∈ {𝑐 ∈ 𝐵 ∣ (𝐹‘𝑐) ∈ (𝐺‘𝑐)}) |
46 | 10, 45 | sseldi 3873 |
. . 3
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ ((𝐹‘𝑧) ∈ (𝐺‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤))))) → 𝑋 ∈ 𝐵) |
47 | | fveq2 6668 |
. . . . . . 7
⊢ (𝑥 = 𝑋 → (𝐹‘𝑥) = (𝐹‘𝑋)) |
48 | | fveq2 6668 |
. . . . . . 7
⊢ (𝑥 = 𝑋 → (𝐺‘𝑥) = (𝐺‘𝑋)) |
49 | 47, 48 | eleq12d 2827 |
. . . . . 6
⊢ (𝑥 = 𝑋 → ((𝐹‘𝑥) ∈ (𝐺‘𝑥) ↔ (𝐹‘𝑋) ∈ (𝐺‘𝑋))) |
50 | | fveq2 6668 |
. . . . . . . 8
⊢ (𝑐 = 𝑥 → (𝐹‘𝑐) = (𝐹‘𝑥)) |
51 | | fveq2 6668 |
. . . . . . . 8
⊢ (𝑐 = 𝑥 → (𝐺‘𝑐) = (𝐺‘𝑥)) |
52 | 50, 51 | eleq12d 2827 |
. . . . . . 7
⊢ (𝑐 = 𝑥 → ((𝐹‘𝑐) ∈ (𝐺‘𝑐) ↔ (𝐹‘𝑥) ∈ (𝐺‘𝑥))) |
53 | 52 | cbvrabv 3392 |
. . . . . 6
⊢ {𝑐 ∈ 𝐵 ∣ (𝐹‘𝑐) ∈ (𝐺‘𝑐)} = {𝑥 ∈ 𝐵 ∣ (𝐹‘𝑥) ∈ (𝐺‘𝑥)} |
54 | 49, 53 | elrab2 3588 |
. . . . 5
⊢ (𝑋 ∈ {𝑐 ∈ 𝐵 ∣ (𝐹‘𝑐) ∈ (𝐺‘𝑐)} ↔ (𝑋 ∈ 𝐵 ∧ (𝐹‘𝑋) ∈ (𝐺‘𝑋))) |
55 | 45, 54 | sylib 221 |
. . . 4
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ ((𝐹‘𝑧) ∈ (𝐺‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤))))) → (𝑋 ∈ 𝐵 ∧ (𝐹‘𝑋) ∈ (𝐺‘𝑋))) |
56 | 55 | simprd 499 |
. . 3
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ ((𝐹‘𝑧) ∈ (𝐺‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤))))) → (𝐹‘𝑋) ∈ (𝐺‘𝑋)) |
57 | | simprrr 782 |
. . . 4
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ ((𝐹‘𝑧) ∈ (𝐺‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤))))) → ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤))) |
58 | 3 | adantr 484 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ ((𝐹‘𝑧) ∈ (𝐺‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤))))) → 𝐴 ∈ On) |
59 | 22 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ ((𝐹‘𝑧) ∈ (𝐺‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤))))) → 𝐺:𝐵⟶𝐴) |
60 | 59, 46 | ffvelrnd 6856 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ ((𝐹‘𝑧) ∈ (𝐺‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤))))) → (𝐺‘𝑋) ∈ 𝐴) |
61 | | onelon 6191 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ On ∧ (𝐺‘𝑋) ∈ 𝐴) → (𝐺‘𝑋) ∈ On) |
62 | 58, 60, 61 | syl2anc 587 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ ((𝐹‘𝑧) ∈ (𝐺‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤))))) → (𝐺‘𝑋) ∈ On) |
63 | | eloni 6176 |
. . . . . . . . . 10
⊢ ((𝐺‘𝑋) ∈ On → Ord (𝐺‘𝑋)) |
64 | | ordirr 6184 |
. . . . . . . . . 10
⊢ (Ord
(𝐺‘𝑋) → ¬ (𝐺‘𝑋) ∈ (𝐺‘𝑋)) |
65 | 62, 63, 64 | 3syl 18 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ ((𝐹‘𝑧) ∈ (𝐺‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤))))) → ¬ (𝐺‘𝑋) ∈ (𝐺‘𝑋)) |
66 | | nelneq 2857 |
. . . . . . . . 9
⊢ (((𝐹‘𝑋) ∈ (𝐺‘𝑋) ∧ ¬ (𝐺‘𝑋) ∈ (𝐺‘𝑋)) → ¬ (𝐹‘𝑋) = (𝐺‘𝑋)) |
67 | 56, 65, 66 | syl2anc 587 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ ((𝐹‘𝑧) ∈ (𝐺‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤))))) → ¬ (𝐹‘𝑋) = (𝐺‘𝑋)) |
68 | | eleq2 2821 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑋 → (𝑧 ∈ 𝑤 ↔ 𝑧 ∈ 𝑋)) |
69 | | fveq2 6668 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑋 → (𝐹‘𝑤) = (𝐹‘𝑋)) |
70 | | fveq2 6668 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑋 → (𝐺‘𝑤) = (𝐺‘𝑋)) |
71 | 69, 70 | eqeq12d 2754 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑋 → ((𝐹‘𝑤) = (𝐺‘𝑤) ↔ (𝐹‘𝑋) = (𝐺‘𝑋))) |
72 | 68, 71 | imbi12d 348 |
. . . . . . . . 9
⊢ (𝑤 = 𝑋 → ((𝑧 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤)) ↔ (𝑧 ∈ 𝑋 → (𝐹‘𝑋) = (𝐺‘𝑋)))) |
73 | 72, 57, 46 | rspcdva 3526 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ ((𝐹‘𝑧) ∈ (𝐺‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤))))) → (𝑧 ∈ 𝑋 → (𝐹‘𝑋) = (𝐺‘𝑋))) |
74 | 67, 73 | mtod 201 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ ((𝐹‘𝑧) ∈ (𝐺‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤))))) → ¬ 𝑧 ∈ 𝑋) |
75 | | ssexg 5188 |
. . . . . . . . . . 11
⊢ (({𝑐 ∈ 𝐵 ∣ (𝐹‘𝑐) ∈ (𝐺‘𝑐)} ⊆ 𝐵 ∧ 𝐵 ∈ On) → {𝑐 ∈ 𝐵 ∣ (𝐹‘𝑐) ∈ (𝐺‘𝑐)} ∈ V) |
76 | 10, 12, 75 | sylancr 590 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ ((𝐹‘𝑧) ∈ (𝐺‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤))))) → {𝑐 ∈ 𝐵 ∣ (𝐹‘𝑐) ∈ (𝐺‘𝑐)} ∈ V) |
77 | | ssonuni 7514 |
. . . . . . . . . 10
⊢ ({𝑐 ∈ 𝐵 ∣ (𝐹‘𝑐) ∈ (𝐺‘𝑐)} ∈ V → ({𝑐 ∈ 𝐵 ∣ (𝐹‘𝑐) ∈ (𝐺‘𝑐)} ⊆ On → ∪ {𝑐
∈ 𝐵 ∣ (𝐹‘𝑐) ∈ (𝐺‘𝑐)} ∈ On)) |
78 | 76, 15, 77 | sylc 65 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ ((𝐹‘𝑧) ∈ (𝐺‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤))))) → ∪
{𝑐 ∈ 𝐵 ∣ (𝐹‘𝑐) ∈ (𝐺‘𝑐)} ∈ On) |
79 | 11, 78 | eqeltrid 2837 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ ((𝐹‘𝑧) ∈ (𝐺‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤))))) → 𝑋 ∈ On) |
80 | | onelon 6191 |
. . . . . . . . 9
⊢ ((𝐵 ∈ On ∧ 𝑧 ∈ 𝐵) → 𝑧 ∈ On) |
81 | 12, 39, 80 | syl2anc 587 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ ((𝐹‘𝑧) ∈ (𝐺‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤))))) → 𝑧 ∈ On) |
82 | | ontri1 6200 |
. . . . . . . 8
⊢ ((𝑋 ∈ On ∧ 𝑧 ∈ On) → (𝑋 ⊆ 𝑧 ↔ ¬ 𝑧 ∈ 𝑋)) |
83 | 79, 81, 82 | syl2anc 587 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ ((𝐹‘𝑧) ∈ (𝐺‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤))))) → (𝑋 ⊆ 𝑧 ↔ ¬ 𝑧 ∈ 𝑋)) |
84 | 74, 83 | mpbird 260 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ ((𝐹‘𝑧) ∈ (𝐺‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤))))) → 𝑋 ⊆ 𝑧) |
85 | | elssuni 4825 |
. . . . . . . 8
⊢ (𝑧 ∈ {𝑐 ∈ 𝐵 ∣ (𝐹‘𝑐) ∈ (𝐺‘𝑐)} → 𝑧 ⊆ ∪ {𝑐 ∈ 𝐵 ∣ (𝐹‘𝑐) ∈ (𝐺‘𝑐)}) |
86 | 85, 11 | sseqtrrdi 3926 |
. . . . . . 7
⊢ (𝑧 ∈ {𝑐 ∈ 𝐵 ∣ (𝐹‘𝑐) ∈ (𝐺‘𝑐)} → 𝑧 ⊆ 𝑋) |
87 | 41, 86 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ ((𝐹‘𝑧) ∈ (𝐺‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤))))) → 𝑧 ⊆ 𝑋) |
88 | 84, 87 | eqssd 3892 |
. . . . 5
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ ((𝐹‘𝑧) ∈ (𝐺‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤))))) → 𝑋 = 𝑧) |
89 | | eleq1 2820 |
. . . . . . 7
⊢ (𝑋 = 𝑧 → (𝑋 ∈ 𝑤 ↔ 𝑧 ∈ 𝑤)) |
90 | 89 | imbi1d 345 |
. . . . . 6
⊢ (𝑋 = 𝑧 → ((𝑋 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤)) ↔ (𝑧 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤)))) |
91 | 90 | ralbidv 3109 |
. . . . 5
⊢ (𝑋 = 𝑧 → (∀𝑤 ∈ 𝐵 (𝑋 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤)) ↔ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤)))) |
92 | 88, 91 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ ((𝐹‘𝑧) ∈ (𝐺‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤))))) → (∀𝑤 ∈ 𝐵 (𝑋 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤)) ↔ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤)))) |
93 | 57, 92 | mpbird 260 |
. . 3
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ ((𝐹‘𝑧) ∈ (𝐺‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤))))) → ∀𝑤 ∈ 𝐵 (𝑋 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤))) |
94 | 46, 56, 93 | 3jca 1129 |
. 2
⊢ ((𝜑 ∧ (𝑧 ∈ 𝐵 ∧ ((𝐹‘𝑧) ∈ (𝐺‘𝑧) ∧ ∀𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤))))) → (𝑋 ∈ 𝐵 ∧ (𝐹‘𝑋) ∈ (𝐺‘𝑋) ∧ ∀𝑤 ∈ 𝐵 (𝑋 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤)))) |
95 | 9, 94 | rexlimddv 3200 |
1
⊢ (𝜑 → (𝑋 ∈ 𝐵 ∧ (𝐹‘𝑋) ∈ (𝐺‘𝑋) ∧ ∀𝑤 ∈ 𝐵 (𝑋 ∈ 𝑤 → (𝐹‘𝑤) = (𝐺‘𝑤)))) |