Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . . . . . . . . . 11
⊢ dom
(𝐴 CNF 𝐵) = dom (𝐴 CNF 𝐵) |
2 | | eldifi 4125 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ (On ∖
2o) → 𝐴
∈ On) |
3 | 2 | adantr 482 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) → 𝐴 ∈
On) |
4 | | simpr 486 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) → 𝐵 ∈
On) |
5 | | eqid 2733 |
. . . . . . . . . . 11
⊢
{〈𝑎, 𝑏〉 ∣ ∃𝑐 ∈ 𝐵 ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥)))} = {〈𝑎, 𝑏〉 ∣ ∃𝑐 ∈ 𝐵 ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥)))} |
6 | 1, 3, 4, 5 | cantnf 9684 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) → (𝐴 CNF
𝐵) Isom {〈𝑎, 𝑏〉 ∣ ∃𝑐 ∈ 𝐵 ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥)))}, E (dom (𝐴 CNF 𝐵), (𝐴 ↑o 𝐵))) |
7 | 6 | adantr 482 |
. . . . . . . . 9
⊢ (((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ 𝐹 ∈
dom (𝐴 CNF 𝐵)) → (𝐴 CNF 𝐵) Isom {〈𝑎, 𝑏〉 ∣ ∃𝑐 ∈ 𝐵 ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥)))}, E (dom (𝐴 CNF 𝐵), (𝐴 ↑o 𝐵))) |
8 | | simpr 486 |
. . . . . . . . 9
⊢ (((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ 𝐹 ∈
dom (𝐴 CNF 𝐵)) → 𝐹 ∈ dom (𝐴 CNF 𝐵)) |
9 | | ondif2 8497 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ (On ∖
2o) ↔ (𝐴
∈ On ∧ 1o ∈ 𝐴)) |
10 | 9 | simprbi 498 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ (On ∖
2o) → 1o ∈ 𝐴) |
11 | | dif20el 8500 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ (On ∖
2o) → ∅ ∈ 𝐴) |
12 | 10, 11 | ifcld 4573 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ (On ∖
2o) → if(𝑦
= 𝐶, 1o,
∅) ∈ 𝐴) |
13 | 12 | ad2antrr 725 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ 𝑦 ∈
𝐵) → if(𝑦 = 𝐶, 1o, ∅) ∈ 𝐴) |
14 | 13 | fmpttd 7110 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) → (𝑦 ∈
𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)):𝐵⟶𝐴) |
15 | 11 | adantr 482 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) → ∅ ∈ 𝐴) |
16 | | eqid 2733 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) = (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) |
17 | 4, 15, 16 | sniffsupp 9391 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) → (𝑦 ∈
𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) finSupp
∅) |
18 | 1, 3, 4 | cantnfs 9657 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) → ((𝑦
∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) ∈ dom (𝐴 CNF 𝐵) ↔ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)):𝐵⟶𝐴 ∧ (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) finSupp
∅))) |
19 | 14, 17, 18 | mpbir2and 712 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) → (𝑦 ∈
𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) ∈ dom (𝐴 CNF 𝐵)) |
20 | 19 | adantr 482 |
. . . . . . . . 9
⊢ (((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ 𝐹 ∈
dom (𝐴 CNF 𝐵)) → (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) ∈ dom (𝐴 CNF 𝐵)) |
21 | | isorel 7318 |
. . . . . . . . 9
⊢ (((𝐴 CNF 𝐵) Isom {〈𝑎, 𝑏〉 ∣ ∃𝑐 ∈ 𝐵 ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥)))}, E (dom (𝐴 CNF 𝐵), (𝐴 ↑o 𝐵)) ∧ (𝐹 ∈ dom (𝐴 CNF 𝐵) ∧ (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) ∈ dom (𝐴 CNF 𝐵))) → (𝐹{〈𝑎, 𝑏〉 ∣ ∃𝑐 ∈ 𝐵 ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥)))} (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) ↔ ((𝐴 CNF 𝐵)‘𝐹) E ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o,
∅))))) |
22 | 7, 8, 20, 21 | syl12anc 836 |
. . . . . . . 8
⊢ (((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ 𝐹 ∈
dom (𝐴 CNF 𝐵)) → (𝐹{〈𝑎, 𝑏〉 ∣ ∃𝑐 ∈ 𝐵 ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥)))} (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) ↔ ((𝐴 CNF 𝐵)‘𝐹) E ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o,
∅))))) |
23 | 22 | adantrl 715 |
. . . . . . 7
⊢ (((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ (𝐶 ∈
On ∧ 𝐹 ∈ dom
(𝐴 CNF 𝐵))) → (𝐹{〈𝑎, 𝑏〉 ∣ ∃𝑐 ∈ 𝐵 ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥)))} (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) ↔ ((𝐴 CNF 𝐵)‘𝐹) E ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o,
∅))))) |
24 | 23 | adantr 482 |
. . . . . 6
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ (𝐶 ∈
On ∧ 𝐹 ∈ dom
(𝐴 CNF 𝐵))) ∧ 𝐶 ∈ 𝐵) → (𝐹{〈𝑎, 𝑏〉 ∣ ∃𝑐 ∈ 𝐵 ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥)))} (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) ↔ ((𝐴 CNF 𝐵)‘𝐹) E ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o,
∅))))) |
25 | | fvexd 6903 |
. . . . . . 7
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ (𝐶 ∈
On ∧ 𝐹 ∈ dom
(𝐴 CNF 𝐵))) ∧ 𝐶 ∈ 𝐵) → ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))) ∈
V) |
26 | | epelg 5580 |
. . . . . . 7
⊢ (((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))) ∈ V →
(((𝐴 CNF 𝐵)‘𝐹) E ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))) ↔ ((𝐴 CNF 𝐵)‘𝐹) ∈ ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o,
∅))))) |
27 | 25, 26 | syl 17 |
. . . . . 6
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ (𝐶 ∈
On ∧ 𝐹 ∈ dom
(𝐴 CNF 𝐵))) ∧ 𝐶 ∈ 𝐵) → (((𝐴 CNF 𝐵)‘𝐹) E ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))) ↔ ((𝐴 CNF 𝐵)‘𝐹) ∈ ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o,
∅))))) |
28 | 2 | ad2antrr 725 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ 𝐶 ∈
𝐵) → 𝐴 ∈ On) |
29 | | simplr 768 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ 𝐶 ∈
𝐵) → 𝐵 ∈ On) |
30 | | fconst6g 6777 |
. . . . . . . . . . . . . . . . . 18
⊢ (∅
∈ 𝐴 → (𝐵 × {∅}):𝐵⟶𝐴) |
31 | 11, 30 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ (On ∖
2o) → (𝐵
× {∅}):𝐵⟶𝐴) |
32 | 31 | adantr 482 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) → (𝐵
× {∅}):𝐵⟶𝐴) |
33 | 4, 15 | fczfsuppd 9377 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) → (𝐵
× {∅}) finSupp ∅) |
34 | 1, 3, 4 | cantnfs 9657 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) → ((𝐵
× {∅}) ∈ dom (𝐴 CNF 𝐵) ↔ ((𝐵 × {∅}):𝐵⟶𝐴 ∧ (𝐵 × {∅}) finSupp
∅))) |
35 | 32, 33, 34 | mpbir2and 712 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) → (𝐵
× {∅}) ∈ dom (𝐴 CNF 𝐵)) |
36 | 35 | adantr 482 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ 𝐶 ∈
𝐵) → (𝐵 × {∅}) ∈ dom
(𝐴 CNF 𝐵)) |
37 | | simpr 486 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ 𝐶 ∈
𝐵) → 𝐶 ∈ 𝐵) |
38 | 10 | ad2antrr 725 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ 𝐶 ∈
𝐵) → 1o
∈ 𝐴) |
39 | | fczsupp0 8173 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐵 × {∅}) supp
∅) = ∅ |
40 | | 0ss 4395 |
. . . . . . . . . . . . . . . 16
⊢ ∅
⊆ 𝐶 |
41 | 39, 40 | eqsstri 4015 |
. . . . . . . . . . . . . . 15
⊢ ((𝐵 × {∅}) supp
∅) ⊆ 𝐶 |
42 | 41 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ 𝐶 ∈
𝐵) → ((𝐵 × {∅}) supp
∅) ⊆ 𝐶) |
43 | | 0ex 5306 |
. . . . . . . . . . . . . . . . . 18
⊢ ∅
∈ V |
44 | 43 | fvconst2 7200 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ 𝐵 → ((𝐵 × {∅})‘𝑦) = ∅) |
45 | 44 | ifeq2d 4547 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ 𝐵 → if(𝑦 = 𝐶, 1o, ((𝐵 × {∅})‘𝑦)) = if(𝑦 = 𝐶, 1o, ∅)) |
46 | 45 | mpteq2ia 5250 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ((𝐵 × {∅})‘𝑦))) = (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) |
47 | 46 | eqcomi 2742 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) = (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ((𝐵 × {∅})‘𝑦))) |
48 | 1, 28, 29, 36, 37, 38, 42, 47 | cantnfp1 9672 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ 𝐶 ∈
𝐵) → ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) ∈ dom (𝐴 CNF 𝐵) ∧ ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))) = (((𝐴 ↑o 𝐶) ·o
1o) +o ((𝐴 CNF 𝐵)‘(𝐵 × {∅}))))) |
49 | 48 | simprd 497 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ 𝐶 ∈
𝐵) → ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))) = (((𝐴 ↑o 𝐶) ·o
1o) +o ((𝐴 CNF 𝐵)‘(𝐵 × {∅})))) |
50 | 49 | adantrl 715 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ (𝐶 ∈
On ∧ 𝐶 ∈ 𝐵)) → ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))) = (((𝐴 ↑o 𝐶) ·o
1o) +o ((𝐴 CNF 𝐵)‘(𝐵 × {∅})))) |
51 | | oecl 8532 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ↑o 𝐶) ∈ On) |
52 | 3, 51 | sylan 581 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ 𝐶 ∈
On) → (𝐴
↑o 𝐶)
∈ On) |
53 | | om1 8538 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ↑o 𝐶) ∈ On → ((𝐴 ↑o 𝐶) ·o
1o) = (𝐴
↑o 𝐶)) |
54 | 52, 53 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ 𝐶 ∈
On) → ((𝐴
↑o 𝐶)
·o 1o) = (𝐴 ↑o 𝐶)) |
55 | 1, 3, 4, 15 | cantnf0 9666 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) → ((𝐴 CNF
𝐵)‘(𝐵 × {∅})) =
∅) |
56 | 55 | adantr 482 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ 𝐶 ∈
On) → ((𝐴 CNF 𝐵)‘(𝐵 × {∅})) =
∅) |
57 | 54, 56 | oveq12d 7422 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ 𝐶 ∈
On) → (((𝐴
↑o 𝐶)
·o 1o) +o ((𝐴 CNF 𝐵)‘(𝐵 × {∅}))) = ((𝐴 ↑o 𝐶) +o ∅)) |
58 | | oa0 8511 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ↑o 𝐶) ∈ On → ((𝐴 ↑o 𝐶) +o ∅) =
(𝐴 ↑o 𝐶)) |
59 | 52, 58 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ 𝐶 ∈
On) → ((𝐴
↑o 𝐶)
+o ∅) = (𝐴
↑o 𝐶)) |
60 | 57, 59 | eqtrd 2773 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ 𝐶 ∈
On) → (((𝐴
↑o 𝐶)
·o 1o) +o ((𝐴 CNF 𝐵)‘(𝐵 × {∅}))) = (𝐴 ↑o 𝐶)) |
61 | 60 | adantrr 716 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ (𝐶 ∈
On ∧ 𝐶 ∈ 𝐵)) → (((𝐴 ↑o 𝐶) ·o 1o)
+o ((𝐴 CNF 𝐵)‘(𝐵 × {∅}))) = (𝐴 ↑o 𝐶)) |
62 | 50, 61 | eqtrd 2773 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ (𝐶 ∈
On ∧ 𝐶 ∈ 𝐵)) → ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))) = (𝐴 ↑o 𝐶)) |
63 | 62 | eleq2d 2820 |
. . . . . . . . 9
⊢ (((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ (𝐶 ∈
On ∧ 𝐶 ∈ 𝐵)) → (((𝐴 CNF 𝐵)‘𝐹) ∈ ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))) ↔ ((𝐴 CNF 𝐵)‘𝐹) ∈ (𝐴 ↑o 𝐶))) |
64 | 63 | exp32 422 |
. . . . . . . 8
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) → (𝐶 ∈
On → (𝐶 ∈ 𝐵 → (((𝐴 CNF 𝐵)‘𝐹) ∈ ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))) ↔ ((𝐴 CNF 𝐵)‘𝐹) ∈ (𝐴 ↑o 𝐶))))) |
65 | 64 | adantrd 493 |
. . . . . . 7
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) → ((𝐶
∈ On ∧ 𝐹 ∈
dom (𝐴 CNF 𝐵)) → (𝐶 ∈ 𝐵 → (((𝐴 CNF 𝐵)‘𝐹) ∈ ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))) ↔ ((𝐴 CNF 𝐵)‘𝐹) ∈ (𝐴 ↑o 𝐶))))) |
66 | 65 | imp31 419 |
. . . . . 6
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ (𝐶 ∈
On ∧ 𝐹 ∈ dom
(𝐴 CNF 𝐵))) ∧ 𝐶 ∈ 𝐵) → (((𝐴 CNF 𝐵)‘𝐹) ∈ ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))) ↔ ((𝐴 CNF 𝐵)‘𝐹) ∈ (𝐴 ↑o 𝐶))) |
67 | 24, 27, 66 | 3bitrrd 306 |
. . . . 5
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ (𝐶 ∈
On ∧ 𝐹 ∈ dom
(𝐴 CNF 𝐵))) ∧ 𝐶 ∈ 𝐵) → (((𝐴 CNF 𝐵)‘𝐹) ∈ (𝐴 ↑o 𝐶) ↔ 𝐹{〈𝑎, 𝑏〉 ∣ ∃𝑐 ∈ 𝐵 ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥)))} (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o,
∅)))) |
68 | | fveq1 6887 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝐹 → (𝑎‘𝑐) = (𝐹‘𝑐)) |
69 | 68 | eleq1d 2819 |
. . . . . . . . . 10
⊢ (𝑎 = 𝐹 → ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ↔ (𝐹‘𝑐) ∈ (𝑏‘𝑐))) |
70 | | fveq1 6887 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 𝐹 → (𝑎‘𝑥) = (𝐹‘𝑥)) |
71 | 70 | eqeq1d 2735 |
. . . . . . . . . . . 12
⊢ (𝑎 = 𝐹 → ((𝑎‘𝑥) = (𝑏‘𝑥) ↔ (𝐹‘𝑥) = (𝑏‘𝑥))) |
72 | 71 | imbi2d 341 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝐹 → ((𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥)) ↔ (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = (𝑏‘𝑥)))) |
73 | 72 | ralbidv 3178 |
. . . . . . . . . 10
⊢ (𝑎 = 𝐹 → (∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥)) ↔ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = (𝑏‘𝑥)))) |
74 | 69, 73 | anbi12d 632 |
. . . . . . . . 9
⊢ (𝑎 = 𝐹 → (((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥))) ↔ ((𝐹‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = (𝑏‘𝑥))))) |
75 | 74 | rexbidv 3179 |
. . . . . . . 8
⊢ (𝑎 = 𝐹 → (∃𝑐 ∈ 𝐵 ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥))) ↔ ∃𝑐 ∈ 𝐵 ((𝐹‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = (𝑏‘𝑥))))) |
76 | | fveq1 6887 |
. . . . . . . . . . 11
⊢ (𝑏 = (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) → (𝑏‘𝑐) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐)) |
77 | 76 | eleq2d 2820 |
. . . . . . . . . 10
⊢ (𝑏 = (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) → ((𝐹‘𝑐) ∈ (𝑏‘𝑐) ↔ (𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐))) |
78 | | fveq1 6887 |
. . . . . . . . . . . . 13
⊢ (𝑏 = (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) → (𝑏‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥)) |
79 | 78 | eqeq2d 2744 |
. . . . . . . . . . . 12
⊢ (𝑏 = (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) → ((𝐹‘𝑥) = (𝑏‘𝑥) ↔ (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥))) |
80 | 79 | imbi2d 341 |
. . . . . . . . . . 11
⊢ (𝑏 = (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) → ((𝑐 ∈ 𝑥 → (𝐹‘𝑥) = (𝑏‘𝑥)) ↔ (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥)))) |
81 | 80 | ralbidv 3178 |
. . . . . . . . . 10
⊢ (𝑏 = (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) →
(∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = (𝑏‘𝑥)) ↔ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥)))) |
82 | 77, 81 | anbi12d 632 |
. . . . . . . . 9
⊢ (𝑏 = (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) → (((𝐹‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = (𝑏‘𝑥))) ↔ ((𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥))))) |
83 | 82 | rexbidv 3179 |
. . . . . . . 8
⊢ (𝑏 = (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) →
(∃𝑐 ∈ 𝐵 ((𝐹‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = (𝑏‘𝑥))) ↔ ∃𝑐 ∈ 𝐵 ((𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥))))) |
84 | 75, 83, 5 | bropabg 42006 |
. . . . . . 7
⊢ (𝐹{〈𝑎, 𝑏〉 ∣ ∃𝑐 ∈ 𝐵 ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥)))} (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) ↔ ((𝐹 ∈ V ∧ (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) ∈ V) ∧
∃𝑐 ∈ 𝐵 ((𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥))))) |
85 | | fveq2 6888 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑐 = 𝐶 → (𝐹‘𝑐) = (𝐹‘𝐶)) |
86 | 85 | adantr 482 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑐 = 𝐶 ∧ 𝑐 ∈ 𝐵) → (𝐹‘𝑐) = (𝐹‘𝐶)) |
87 | | eqeq1 2737 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = 𝑐 → (𝑦 = 𝐶 ↔ 𝑐 = 𝐶)) |
88 | 87 | ifbid 4550 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = 𝑐 → if(𝑦 = 𝐶, 1o, ∅) = if(𝑐 = 𝐶, 1o, ∅)) |
89 | | 1oex 8471 |
. . . . . . . . . . . . . . . . . . . 20
⊢
1o ∈ V |
90 | 89, 43 | ifex 4577 |
. . . . . . . . . . . . . . . . . . 19
⊢ if(𝑐 = 𝐶, 1o, ∅) ∈
V |
91 | 88, 16, 90 | fvmpt 6994 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑐 ∈ 𝐵 → ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐) = if(𝑐 = 𝐶, 1o, ∅)) |
92 | | iftrue 4533 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑐 = 𝐶 → if(𝑐 = 𝐶, 1o, ∅) =
1o) |
93 | 91, 92 | sylan9eqr 2795 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑐 = 𝐶 ∧ 𝑐 ∈ 𝐵) → ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐) =
1o) |
94 | 86, 93 | eleq12d 2828 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑐 = 𝐶 ∧ 𝑐 ∈ 𝐵) → ((𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐) ↔ (𝐹‘𝐶) ∈ 1o)) |
95 | | el1o 8490 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹‘𝐶) ∈ 1o ↔ (𝐹‘𝐶) = ∅) |
96 | 95 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑐 = 𝐶 ∧ 𝑐 ∈ 𝐵) → ((𝐹‘𝐶) ∈ 1o ↔ (𝐹‘𝐶) = ∅)) |
97 | 96 | biimpd 228 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑐 = 𝐶 ∧ 𝑐 ∈ 𝐵) → ((𝐹‘𝐶) ∈ 1o → (𝐹‘𝐶) = ∅)) |
98 | | simpl 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑐 = 𝐶 ∧ 𝑐 ∈ 𝐵) → 𝑐 = 𝐶) |
99 | 97, 98 | jctild 527 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑐 = 𝐶 ∧ 𝑐 ∈ 𝐵) → ((𝐹‘𝐶) ∈ 1o → (𝑐 = 𝐶 ∧ (𝐹‘𝐶) = ∅))) |
100 | 94, 99 | sylbid 239 |
. . . . . . . . . . . . . . 15
⊢ ((𝑐 = 𝐶 ∧ 𝑐 ∈ 𝐵) → ((𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐) → (𝑐 = 𝐶 ∧ (𝐹‘𝐶) = ∅))) |
101 | 100 | expimpd 455 |
. . . . . . . . . . . . . 14
⊢ (𝑐 = 𝐶 → ((𝑐 ∈ 𝐵 ∧ (𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐)) → (𝑐 = 𝐶 ∧ (𝐹‘𝐶) = ∅))) |
102 | 91 | adantl 483 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑐 ≠ 𝐶 ∧ 𝑐 ∈ 𝐵) → ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐) = if(𝑐 = 𝐶, 1o, ∅)) |
103 | | simpl 484 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑐 ≠ 𝐶 ∧ 𝑐 ∈ 𝐵) → 𝑐 ≠ 𝐶) |
104 | 103 | neneqd 2946 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑐 ≠ 𝐶 ∧ 𝑐 ∈ 𝐵) → ¬ 𝑐 = 𝐶) |
105 | 104 | iffalsed 4538 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑐 ≠ 𝐶 ∧ 𝑐 ∈ 𝐵) → if(𝑐 = 𝐶, 1o, ∅) =
∅) |
106 | 102, 105 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑐 ≠ 𝐶 ∧ 𝑐 ∈ 𝐵) → ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐) = ∅) |
107 | 106 | eleq2d 2820 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑐 ≠ 𝐶 ∧ 𝑐 ∈ 𝐵) → ((𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐) ↔ (𝐹‘𝑐) ∈ ∅)) |
108 | 107 | biimpd 228 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑐 ≠ 𝐶 ∧ 𝑐 ∈ 𝐵) → ((𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐) → (𝐹‘𝑐) ∈ ∅)) |
109 | 108 | expimpd 455 |
. . . . . . . . . . . . . . 15
⊢ (𝑐 ≠ 𝐶 → ((𝑐 ∈ 𝐵 ∧ (𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐)) → (𝐹‘𝑐) ∈ ∅)) |
110 | | noel 4329 |
. . . . . . . . . . . . . . . 16
⊢ ¬
(𝐹‘𝑐) ∈ ∅ |
111 | 110 | pm2.21i 119 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹‘𝑐) ∈ ∅ → (𝑐 = 𝐶 ∧ (𝐹‘𝐶) = ∅)) |
112 | 109, 111 | syl6 35 |
. . . . . . . . . . . . . 14
⊢ (𝑐 ≠ 𝐶 → ((𝑐 ∈ 𝐵 ∧ (𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐)) → (𝑐 = 𝐶 ∧ (𝐹‘𝐶) = ∅))) |
113 | 101, 112 | pm2.61ine 3026 |
. . . . . . . . . . . . 13
⊢ ((𝑐 ∈ 𝐵 ∧ (𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐)) → (𝑐 = 𝐶 ∧ (𝐹‘𝐶) = ∅)) |
114 | 113 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ 𝐶 ∈
On) ∧ 𝐶 ∈ 𝐵) → ((𝑐 ∈ 𝐵 ∧ (𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐)) → (𝑐 = 𝐶 ∧ (𝐹‘𝐶) = ∅))) |
115 | | fveqeq2 6897 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝐶 → ((𝐹‘𝑥) = ∅ ↔ (𝐹‘𝐶) = ∅)) |
116 | 115 | ralsng 4676 |
. . . . . . . . . . . . . . 15
⊢ (𝐶 ∈ 𝐵 → (∀𝑥 ∈ {𝐶} (𝐹‘𝑥) = ∅ ↔ (𝐹‘𝐶) = ∅)) |
117 | 116 | anbi2d 630 |
. . . . . . . . . . . . . 14
⊢ (𝐶 ∈ 𝐵 → ((𝑐 = 𝐶 ∧ ∀𝑥 ∈ {𝐶} (𝐹‘𝑥) = ∅) ↔ (𝑐 = 𝐶 ∧ (𝐹‘𝐶) = ∅))) |
118 | 117 | biimprd 247 |
. . . . . . . . . . . . 13
⊢ (𝐶 ∈ 𝐵 → ((𝑐 = 𝐶 ∧ (𝐹‘𝐶) = ∅) → (𝑐 = 𝐶 ∧ ∀𝑥 ∈ {𝐶} (𝐹‘𝑥) = ∅))) |
119 | 118 | adantl 483 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ 𝐶 ∈
On) ∧ 𝐶 ∈ 𝐵) → ((𝑐 = 𝐶 ∧ (𝐹‘𝐶) = ∅) → (𝑐 = 𝐶 ∧ ∀𝑥 ∈ {𝐶} (𝐹‘𝑥) = ∅))) |
120 | 4 | anim1i 616 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ 𝐶 ∈
On) → (𝐵 ∈ On
∧ 𝐶 ∈
On)) |
121 | 120 | adantr 482 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ 𝐶 ∈
On) ∧ 𝐶 ∈ 𝐵) → (𝐵 ∈ On ∧ 𝐶 ∈ On)) |
122 | | pm3.31 451 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ 𝐵 → (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥))) → ((𝑥 ∈ 𝐵 ∧ 𝑐 ∈ 𝑥) → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥))) |
123 | 122 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) → ((𝑥 ∈ 𝐵 → (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥))) → ((𝑥 ∈ 𝐵 ∧ 𝑐 ∈ 𝑥) → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥)))) |
124 | | eldif 3957 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ (𝐵 ∖ suc 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ suc 𝐶)) |
125 | | simplr 768 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ 𝐵) → 𝑐 = 𝐶) |
126 | 125 | eleq1d 2819 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ 𝐵) → (𝑐 ∈ 𝑥 ↔ 𝐶 ∈ 𝑥)) |
127 | | simpl 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐵 ∈ On ∧ 𝐶 ∈ On) → 𝐵 ∈ On) |
128 | 127 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) → 𝐵 ∈ On) |
129 | | onelon 6386 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐵 ∈ On ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ On) |
130 | 128, 129 | sylan 581 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ On) |
131 | | simpllr 775 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ 𝐵) → 𝐶 ∈ On) |
132 | | ontri1 6395 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑥 ∈ On ∧ 𝐶 ∈ On) → (𝑥 ⊆ 𝐶 ↔ ¬ 𝐶 ∈ 𝑥)) |
133 | 130, 131,
132 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ 𝐵) → (𝑥 ⊆ 𝐶 ↔ ¬ 𝐶 ∈ 𝑥)) |
134 | 133 | con2bid 355 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ 𝐵) → (𝐶 ∈ 𝑥 ↔ ¬ 𝑥 ⊆ 𝐶)) |
135 | | onsssuc 6451 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑥 ∈ On ∧ 𝐶 ∈ On) → (𝑥 ⊆ 𝐶 ↔ 𝑥 ∈ suc 𝐶)) |
136 | 130, 131,
135 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ 𝐵) → (𝑥 ⊆ 𝐶 ↔ 𝑥 ∈ suc 𝐶)) |
137 | 136 | notbid 318 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ 𝐵) → (¬ 𝑥 ⊆ 𝐶 ↔ ¬ 𝑥 ∈ suc 𝐶)) |
138 | 126, 134,
137 | 3bitrrd 306 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ 𝐵) → (¬ 𝑥 ∈ suc 𝐶 ↔ 𝑐 ∈ 𝑥)) |
139 | 138 | pm5.32da 580 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) → ((𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ suc 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ 𝑐 ∈ 𝑥))) |
140 | 124, 139 | bitrid 283 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) → (𝑥 ∈ (𝐵 ∖ suc 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ 𝑐 ∈ 𝑥))) |
141 | 140 | biimpd 228 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) → (𝑥 ∈ (𝐵 ∖ suc 𝐶) → (𝑥 ∈ 𝐵 ∧ 𝑐 ∈ 𝑥))) |
142 | 141 | imim1d 82 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) → (((𝑥 ∈ 𝐵 ∧ 𝑐 ∈ 𝑥) → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥)) → (𝑥 ∈ (𝐵 ∖ suc 𝐶) → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥)))) |
143 | | eldifi 4125 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 ∈ (𝐵 ∖ suc 𝐶) → 𝑥 ∈ 𝐵) |
144 | 143 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ (𝐵 ∖ suc 𝐶)) → 𝑥 ∈ 𝐵) |
145 | | eqeq1 2737 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑦 = 𝑥 → (𝑦 = 𝐶 ↔ 𝑥 = 𝐶)) |
146 | 145 | ifbid 4550 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦 = 𝑥 → if(𝑦 = 𝐶, 1o, ∅) = if(𝑥 = 𝐶, 1o, ∅)) |
147 | 89, 43 | ifex 4577 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ if(𝑥 = 𝐶, 1o, ∅) ∈
V |
148 | 146, 16, 147 | fvmpt 6994 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 ∈ 𝐵 → ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥) = if(𝑥 = 𝐶, 1o, ∅)) |
149 | 144, 148 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ (𝐵 ∖ suc 𝐶)) → ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥) = if(𝑥 = 𝐶, 1o, ∅)) |
150 | 128, 143,
129 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ (𝐵 ∖ suc 𝐶)) → 𝑥 ∈ On) |
151 | | eloni 6371 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑥 ∈ On → Ord 𝑥) |
152 | 150, 151 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ (𝐵 ∖ suc 𝐶)) → Ord 𝑥) |
153 | | eloni 6371 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝐵 ∈ On → Ord 𝐵) |
154 | 153 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) → Ord 𝐵) |
155 | | simplr 768 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) → 𝐶 ∈ On) |
156 | | ordeldifsucon 41942 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((Ord
𝐵 ∧ 𝐶 ∈ On) → (𝑥 ∈ (𝐵 ∖ suc 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ 𝐶 ∈ 𝑥))) |
157 | 154, 155,
156 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) → (𝑥 ∈ (𝐵 ∖ suc 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ 𝐶 ∈ 𝑥))) |
158 | 157 | biimpa 478 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ (𝐵 ∖ suc 𝐶)) → (𝑥 ∈ 𝐵 ∧ 𝐶 ∈ 𝑥)) |
159 | | ordirr 6379 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (Ord
𝑥 → ¬ 𝑥 ∈ 𝑥) |
160 | | eleq1 2822 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑥 = 𝐶 → (𝑥 ∈ 𝑥 ↔ 𝐶 ∈ 𝑥)) |
161 | 160 | notbid 318 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑥 = 𝐶 → (¬ 𝑥 ∈ 𝑥 ↔ ¬ 𝐶 ∈ 𝑥)) |
162 | 159, 161 | syl5ibcom 244 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (Ord
𝑥 → (𝑥 = 𝐶 → ¬ 𝐶 ∈ 𝑥)) |
163 | 162 | con2d 134 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (Ord
𝑥 → (𝐶 ∈ 𝑥 → ¬ 𝑥 = 𝐶)) |
164 | 163 | adantld 492 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (Ord
𝑥 → ((𝑥 ∈ 𝐵 ∧ 𝐶 ∈ 𝑥) → ¬ 𝑥 = 𝐶)) |
165 | 152, 158,
164 | sylc 65 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ (𝐵 ∖ suc 𝐶)) → ¬ 𝑥 = 𝐶) |
166 | 165 | iffalsed 4538 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ (𝐵 ∖ suc 𝐶)) → if(𝑥 = 𝐶, 1o, ∅) =
∅) |
167 | 149, 166 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ (𝐵 ∖ suc 𝐶)) → ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥) = ∅) |
168 | 167 | eqeq2d 2744 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ (𝐵 ∖ suc 𝐶)) → ((𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥) ↔ (𝐹‘𝑥) = ∅)) |
169 | 168 | biimpd 228 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ (𝐵 ∖ suc 𝐶)) → ((𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥) → (𝐹‘𝑥) = ∅)) |
170 | 169 | ex 414 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) → (𝑥 ∈ (𝐵 ∖ suc 𝐶) → ((𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥) → (𝐹‘𝑥) = ∅))) |
171 | 170 | a2d 29 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) → ((𝑥 ∈ (𝐵 ∖ suc 𝐶) → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥)) → (𝑥 ∈ (𝐵 ∖ suc 𝐶) → (𝐹‘𝑥) = ∅))) |
172 | 123, 142,
171 | 3syld 60 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) → ((𝑥 ∈ 𝐵 → (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥))) → (𝑥 ∈ (𝐵 ∖ suc 𝐶) → (𝐹‘𝑥) = ∅))) |
173 | 172 | ralimdv2 3164 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) → (∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥)) → ∀𝑥 ∈ (𝐵 ∖ suc 𝐶)(𝐹‘𝑥) = ∅)) |
174 | 121, 173 | sylan 581 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐴 ∈ (On
∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) ∧ 𝑐 = 𝐶) → (∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥)) → ∀𝑥 ∈ (𝐵 ∖ suc 𝐶)(𝐹‘𝑥) = ∅)) |
175 | 174 | adantr 482 |
. . . . . . . . . . . . . 14
⊢
((((((𝐴 ∈ (On
∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) ∧ 𝑐 = 𝐶) ∧ ∀𝑥 ∈ {𝐶} (𝐹‘𝑥) = ∅) → (∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥)) → ∀𝑥 ∈ (𝐵 ∖ suc 𝐶)(𝐹‘𝑥) = ∅)) |
176 | | ralun 4191 |
. . . . . . . . . . . . . . . . 17
⊢
((∀𝑥 ∈
{𝐶} (𝐹‘𝑥) = ∅ ∧ ∀𝑥 ∈ (𝐵 ∖ suc 𝐶)(𝐹‘𝑥) = ∅) → ∀𝑥 ∈ ({𝐶} ∪ (𝐵 ∖ suc 𝐶))(𝐹‘𝑥) = ∅) |
177 | 176 | adantll 713 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝐴 ∈ (On
∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) ∧ 𝑐 = 𝐶) ∧ ∀𝑥 ∈ {𝐶} (𝐹‘𝑥) = ∅) ∧ ∀𝑥 ∈ (𝐵 ∖ suc 𝐶)(𝐹‘𝑥) = ∅) → ∀𝑥 ∈ ({𝐶} ∪ (𝐵 ∖ suc 𝐶))(𝐹‘𝑥) = ∅) |
178 | | undif3 4289 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ({𝐶} ∪ (𝐵 ∖ suc 𝐶)) = (({𝐶} ∪ 𝐵) ∖ (suc 𝐶 ∖ {𝐶})) |
179 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐶 ∈ On ∧ 𝐶 ∈ 𝐵) → 𝐶 ∈ 𝐵) |
180 | 179 | snssd 4811 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐶 ∈ On ∧ 𝐶 ∈ 𝐵) → {𝐶} ⊆ 𝐵) |
181 | | ssequn1 4179 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ({𝐶} ⊆ 𝐵 ↔ ({𝐶} ∪ 𝐵) = 𝐵) |
182 | 180, 181 | sylib 217 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐶 ∈ On ∧ 𝐶 ∈ 𝐵) → ({𝐶} ∪ 𝐵) = 𝐵) |
183 | | simpl 484 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐶 ∈ On ∧ 𝐶 ∈ 𝐵) → 𝐶 ∈ On) |
184 | | eloni 6371 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐶 ∈ On → Ord 𝐶) |
185 | | orddif 6457 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (Ord
𝐶 → 𝐶 = (suc 𝐶 ∖ {𝐶})) |
186 | 183, 184,
185 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐶 ∈ On ∧ 𝐶 ∈ 𝐵) → 𝐶 = (suc 𝐶 ∖ {𝐶})) |
187 | 186 | eqcomd 2739 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐶 ∈ On ∧ 𝐶 ∈ 𝐵) → (suc 𝐶 ∖ {𝐶}) = 𝐶) |
188 | 182, 187 | difeq12d 4122 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐶 ∈ On ∧ 𝐶 ∈ 𝐵) → (({𝐶} ∪ 𝐵) ∖ (suc 𝐶 ∖ {𝐶})) = (𝐵 ∖ 𝐶)) |
189 | 178, 188 | eqtrid 2785 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐶 ∈ On ∧ 𝐶 ∈ 𝐵) → ({𝐶} ∪ (𝐵 ∖ suc 𝐶)) = (𝐵 ∖ 𝐶)) |
190 | 189 | adantll 713 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ 𝐶 ∈
On) ∧ 𝐶 ∈ 𝐵) → ({𝐶} ∪ (𝐵 ∖ suc 𝐶)) = (𝐵 ∖ 𝐶)) |
191 | 190 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐴 ∈ (On
∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) ∧ 𝑐 = 𝐶) → ({𝐶} ∪ (𝐵 ∖ suc 𝐶)) = (𝐵 ∖ 𝐶)) |
192 | 191 | raleqdv 3326 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐴 ∈ (On
∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) ∧ 𝑐 = 𝐶) → (∀𝑥 ∈ ({𝐶} ∪ (𝐵 ∖ suc 𝐶))(𝐹‘𝑥) = ∅ ↔ ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅)) |
193 | 192 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝐴 ∈ (On
∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) ∧ 𝑐 = 𝐶) ∧ ∀𝑥 ∈ {𝐶} (𝐹‘𝑥) = ∅) ∧ ∀𝑥 ∈ (𝐵 ∖ suc 𝐶)(𝐹‘𝑥) = ∅) → (∀𝑥 ∈ ({𝐶} ∪ (𝐵 ∖ suc 𝐶))(𝐹‘𝑥) = ∅ ↔ ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅)) |
194 | 177, 193 | mpbid 231 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝐴 ∈ (On
∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) ∧ 𝑐 = 𝐶) ∧ ∀𝑥 ∈ {𝐶} (𝐹‘𝑥) = ∅) ∧ ∀𝑥 ∈ (𝐵 ∖ suc 𝐶)(𝐹‘𝑥) = ∅) → ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅) |
195 | 194 | ex 414 |
. . . . . . . . . . . . . 14
⊢
((((((𝐴 ∈ (On
∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) ∧ 𝑐 = 𝐶) ∧ ∀𝑥 ∈ {𝐶} (𝐹‘𝑥) = ∅) → (∀𝑥 ∈ (𝐵 ∖ suc 𝐶)(𝐹‘𝑥) = ∅ → ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅)) |
196 | 175, 195 | syld 47 |
. . . . . . . . . . . . 13
⊢
((((((𝐴 ∈ (On
∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) ∧ 𝑐 = 𝐶) ∧ ∀𝑥 ∈ {𝐶} (𝐹‘𝑥) = ∅) → (∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥)) → ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅)) |
197 | 196 | expl 459 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ 𝐶 ∈
On) ∧ 𝐶 ∈ 𝐵) → ((𝑐 = 𝐶 ∧ ∀𝑥 ∈ {𝐶} (𝐹‘𝑥) = ∅) → (∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥)) → ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅))) |
198 | 114, 119,
197 | 3syld 60 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ 𝐶 ∈
On) ∧ 𝐶 ∈ 𝐵) → ((𝑐 ∈ 𝐵 ∧ (𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐)) → (∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥)) → ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅))) |
199 | 198 | expdimp 454 |
. . . . . . . . . 10
⊢
(((((𝐴 ∈ (On
∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) → ((𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐) → (∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥)) → ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅))) |
200 | 199 | impd 412 |
. . . . . . . . 9
⊢
(((((𝐴 ∈ (On
∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) → (((𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥))) → ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅)) |
201 | 200 | rexlimdva 3156 |
. . . . . . . 8
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ 𝐶 ∈
On) ∧ 𝐶 ∈ 𝐵) → (∃𝑐 ∈ 𝐵 ((𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥))) → ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅)) |
202 | 201 | adantld 492 |
. . . . . . 7
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ 𝐶 ∈
On) ∧ 𝐶 ∈ 𝐵) → (((𝐹 ∈ V ∧ (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) ∈ V) ∧
∃𝑐 ∈ 𝐵 ((𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥)))) → ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅)) |
203 | 84, 202 | biimtrid 241 |
. . . . . 6
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ 𝐶 ∈
On) ∧ 𝐶 ∈ 𝐵) → (𝐹{〈𝑎, 𝑏〉 ∣ ∃𝑐 ∈ 𝐵 ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥)))} (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) →
∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅)) |
204 | 203 | adantlrr 720 |
. . . . 5
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ (𝐶 ∈
On ∧ 𝐹 ∈ dom
(𝐴 CNF 𝐵))) ∧ 𝐶 ∈ 𝐵) → (𝐹{〈𝑎, 𝑏〉 ∣ ∃𝑐 ∈ 𝐵 ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥)))} (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) →
∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅)) |
205 | 67, 204 | sylbid 239 |
. . . 4
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ (𝐶 ∈
On ∧ 𝐹 ∈ dom
(𝐴 CNF 𝐵))) ∧ 𝐶 ∈ 𝐵) → (((𝐴 CNF 𝐵)‘𝐹) ∈ (𝐴 ↑o 𝐶) → ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅)) |
206 | 205 | ex 414 |
. . 3
⊢ (((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ (𝐶 ∈
On ∧ 𝐹 ∈ dom
(𝐴 CNF 𝐵))) → (𝐶 ∈ 𝐵 → (((𝐴 CNF 𝐵)‘𝐹) ∈ (𝐴 ↑o 𝐶) → ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅))) |
207 | | ral0 4511 |
. . . . 5
⊢
∀𝑥 ∈
∅ (𝐹‘𝑥) = ∅ |
208 | | ssdif0 4362 |
. . . . . . 7
⊢ (𝐵 ⊆ 𝐶 ↔ (𝐵 ∖ 𝐶) = ∅) |
209 | 208 | biimpi 215 |
. . . . . 6
⊢ (𝐵 ⊆ 𝐶 → (𝐵 ∖ 𝐶) = ∅) |
210 | 209 | raleqdv 3326 |
. . . . 5
⊢ (𝐵 ⊆ 𝐶 → (∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅ ↔ ∀𝑥 ∈ ∅ (𝐹‘𝑥) = ∅)) |
211 | 207, 210 | mpbiri 258 |
. . . 4
⊢ (𝐵 ⊆ 𝐶 → ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅) |
212 | 211 | a1i13 27 |
. . 3
⊢ (((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ (𝐶 ∈
On ∧ 𝐹 ∈ dom
(𝐴 CNF 𝐵))) → (𝐵 ⊆ 𝐶 → (((𝐴 CNF 𝐵)‘𝐹) ∈ (𝐴 ↑o 𝐶) → ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅))) |
213 | 184 | adantr 482 |
. . . 4
⊢ ((𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵)) → Ord 𝐶) |
214 | 153 | adantl 483 |
. . . 4
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) → Ord 𝐵) |
215 | | ordtri2or 6459 |
. . . 4
⊢ ((Ord
𝐶 ∧ Ord 𝐵) → (𝐶 ∈ 𝐵 ∨ 𝐵 ⊆ 𝐶)) |
216 | 213, 214,
215 | syl2anr 598 |
. . 3
⊢ (((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ (𝐶 ∈
On ∧ 𝐹 ∈ dom
(𝐴 CNF 𝐵))) → (𝐶 ∈ 𝐵 ∨ 𝐵 ⊆ 𝐶)) |
217 | 206, 212,
216 | mpjaod 859 |
. 2
⊢ (((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ (𝐶 ∈
On ∧ 𝐹 ∈ dom
(𝐴 CNF 𝐵))) → (((𝐴 CNF 𝐵)‘𝐹) ∈ (𝐴 ↑o 𝐶) → ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅)) |
218 | 3 | ad2antrr 725 |
. . . 4
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ (𝐶 ∈
On ∧ 𝐹 ∈ dom
(𝐴 CNF 𝐵))) ∧ ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅) → 𝐴 ∈ On) |
219 | | simpllr 775 |
. . . 4
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ (𝐶 ∈
On ∧ 𝐹 ∈ dom
(𝐴 CNF 𝐵))) ∧ ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅) → 𝐵 ∈ On) |
220 | | simplrr 777 |
. . . 4
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ (𝐶 ∈
On ∧ 𝐹 ∈ dom
(𝐴 CNF 𝐵))) ∧ ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅) → 𝐹 ∈ dom (𝐴 CNF 𝐵)) |
221 | 15 | ad2antrr 725 |
. . . 4
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ (𝐶 ∈
On ∧ 𝐹 ∈ dom
(𝐴 CNF 𝐵))) ∧ ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅) → ∅ ∈ 𝐴) |
222 | | simplrl 776 |
. . . 4
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ (𝐶 ∈
On ∧ 𝐹 ∈ dom
(𝐴 CNF 𝐵))) ∧ ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅) → 𝐶 ∈ On) |
223 | 1, 3, 4 | cantnfs 9657 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) → (𝐹 ∈
dom (𝐴 CNF 𝐵) ↔ (𝐹:𝐵⟶𝐴 ∧ 𝐹 finSupp ∅))) |
224 | 223 | biimpd 228 |
. . . . . . . . 9
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) → (𝐹 ∈
dom (𝐴 CNF 𝐵) → (𝐹:𝐵⟶𝐴 ∧ 𝐹 finSupp ∅))) |
225 | 224 | adantld 492 |
. . . . . . . 8
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) → ((𝐶
∈ On ∧ 𝐹 ∈
dom (𝐴 CNF 𝐵)) → (𝐹:𝐵⟶𝐴 ∧ 𝐹 finSupp ∅))) |
226 | 225 | imp 408 |
. . . . . . 7
⊢ (((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ (𝐶 ∈
On ∧ 𝐹 ∈ dom
(𝐴 CNF 𝐵))) → (𝐹:𝐵⟶𝐴 ∧ 𝐹 finSupp ∅)) |
227 | 226 | simpld 496 |
. . . . . 6
⊢ (((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ (𝐶 ∈
On ∧ 𝐹 ∈ dom
(𝐴 CNF 𝐵))) → 𝐹:𝐵⟶𝐴) |
228 | 227 | adantr 482 |
. . . . 5
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ (𝐶 ∈
On ∧ 𝐹 ∈ dom
(𝐴 CNF 𝐵))) ∧ ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅) → 𝐹:𝐵⟶𝐴) |
229 | | fveqeq2 6897 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → ((𝐹‘𝑥) = ∅ ↔ (𝐹‘𝑦) = ∅)) |
230 | 229 | rspccv 3609 |
. . . . . . 7
⊢
(∀𝑥 ∈
(𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅ → (𝑦 ∈ (𝐵 ∖ 𝐶) → (𝐹‘𝑦) = ∅)) |
231 | 230 | adantl 483 |
. . . . . 6
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ (𝐶 ∈
On ∧ 𝐹 ∈ dom
(𝐴 CNF 𝐵))) ∧ ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅) → (𝑦 ∈ (𝐵 ∖ 𝐶) → (𝐹‘𝑦) = ∅)) |
232 | 231 | imp 408 |
. . . . 5
⊢
(((((𝐴 ∈ (On
∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) ∧ ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅) ∧ 𝑦 ∈ (𝐵 ∖ 𝐶)) → (𝐹‘𝑦) = ∅) |
233 | 228, 232 | suppss 8174 |
. . . 4
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ (𝐶 ∈
On ∧ 𝐹 ∈ dom
(𝐴 CNF 𝐵))) ∧ ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅) → (𝐹 supp ∅) ⊆ 𝐶) |
234 | 1, 218, 219, 220, 221, 222, 233 | cantnflt2 9664 |
. . 3
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ (𝐶 ∈
On ∧ 𝐹 ∈ dom
(𝐴 CNF 𝐵))) ∧ ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅) → ((𝐴 CNF 𝐵)‘𝐹) ∈ (𝐴 ↑o 𝐶)) |
235 | 234 | ex 414 |
. 2
⊢ (((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ (𝐶 ∈
On ∧ 𝐹 ∈ dom
(𝐴 CNF 𝐵))) → (∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅ → ((𝐴 CNF 𝐵)‘𝐹) ∈ (𝐴 ↑o 𝐶))) |
236 | 217, 235 | impbid 211 |
1
⊢ (((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ (𝐶 ∈
On ∧ 𝐹 ∈ dom
(𝐴 CNF 𝐵))) → (((𝐴 CNF 𝐵)‘𝐹) ∈ (𝐴 ↑o 𝐶) ↔ ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅)) |