| Step | Hyp | Ref
| Expression |
| 1 | | eqid 2737 |
. . . . . . . . . . 11
⊢ dom
(𝐴 CNF 𝐵) = dom (𝐴 CNF 𝐵) |
| 2 | | eldifi 4131 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ (On ∖
2o) → 𝐴
∈ On) |
| 3 | 2 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) → 𝐴 ∈
On) |
| 4 | | simpr 484 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) → 𝐵 ∈
On) |
| 5 | | eqid 2737 |
. . . . . . . . . . 11
⊢
{〈𝑎, 𝑏〉 ∣ ∃𝑐 ∈ 𝐵 ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥)))} = {〈𝑎, 𝑏〉 ∣ ∃𝑐 ∈ 𝐵 ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥)))} |
| 6 | 1, 3, 4, 5 | cantnf 9733 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) → (𝐴 CNF
𝐵) Isom {〈𝑎, 𝑏〉 ∣ ∃𝑐 ∈ 𝐵 ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥)))}, E (dom (𝐴 CNF 𝐵), (𝐴 ↑o 𝐵))) |
| 7 | 6 | adantr 480 |
. . . . . . . . 9
⊢ (((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ 𝐹 ∈
dom (𝐴 CNF 𝐵)) → (𝐴 CNF 𝐵) Isom {〈𝑎, 𝑏〉 ∣ ∃𝑐 ∈ 𝐵 ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥)))}, E (dom (𝐴 CNF 𝐵), (𝐴 ↑o 𝐵))) |
| 8 | | simpr 484 |
. . . . . . . . 9
⊢ (((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ 𝐹 ∈
dom (𝐴 CNF 𝐵)) → 𝐹 ∈ dom (𝐴 CNF 𝐵)) |
| 9 | | ondif2 8540 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ (On ∖
2o) ↔ (𝐴
∈ On ∧ 1o ∈ 𝐴)) |
| 10 | 9 | simprbi 496 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ (On ∖
2o) → 1o ∈ 𝐴) |
| 11 | | dif20el 8543 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ (On ∖
2o) → ∅ ∈ 𝐴) |
| 12 | 10, 11 | ifcld 4572 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ (On ∖
2o) → if(𝑦
= 𝐶, 1o,
∅) ∈ 𝐴) |
| 13 | 12 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ 𝑦 ∈
𝐵) → if(𝑦 = 𝐶, 1o, ∅) ∈ 𝐴) |
| 14 | 13 | fmpttd 7135 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) → (𝑦 ∈
𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)):𝐵⟶𝐴) |
| 15 | 11 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) → ∅ ∈ 𝐴) |
| 16 | | eqid 2737 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) = (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) |
| 17 | 4, 15, 16 | sniffsupp 9440 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) → (𝑦 ∈
𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) finSupp
∅) |
| 18 | 1, 3, 4 | cantnfs 9706 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) → ((𝑦
∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) ∈ dom (𝐴 CNF 𝐵) ↔ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)):𝐵⟶𝐴 ∧ (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) finSupp
∅))) |
| 19 | 14, 17, 18 | mpbir2and 713 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) → (𝑦 ∈
𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) ∈ dom (𝐴 CNF 𝐵)) |
| 20 | 19 | adantr 480 |
. . . . . . . . 9
⊢ (((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ 𝐹 ∈
dom (𝐴 CNF 𝐵)) → (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) ∈ dom (𝐴 CNF 𝐵)) |
| 21 | | isorel 7346 |
. . . . . . . . 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 837 |
. . . . . . . 8
⊢ (((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ 𝐹 ∈
dom (𝐴 CNF 𝐵)) → (𝐹{〈𝑎, 𝑏〉 ∣ ∃𝑐 ∈ 𝐵 ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥)))} (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) ↔ ((𝐴 CNF 𝐵)‘𝐹) E ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o,
∅))))) |
| 23 | 22 | adantrl 716 |
. . . . . . 7
⊢ (((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ (𝐶 ∈
On ∧ 𝐹 ∈ dom
(𝐴 CNF 𝐵))) → (𝐹{〈𝑎, 𝑏〉 ∣ ∃𝑐 ∈ 𝐵 ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥)))} (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) ↔ ((𝐴 CNF 𝐵)‘𝐹) E ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o,
∅))))) |
| 24 | 23 | adantr 480 |
. . . . . 6
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ (𝐶 ∈
On ∧ 𝐹 ∈ dom
(𝐴 CNF 𝐵))) ∧ 𝐶 ∈ 𝐵) → (𝐹{〈𝑎, 𝑏〉 ∣ ∃𝑐 ∈ 𝐵 ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥)))} (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) ↔ ((𝐴 CNF 𝐵)‘𝐹) E ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o,
∅))))) |
| 25 | | fvexd 6921 |
. . . . . . 7
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ (𝐶 ∈
On ∧ 𝐹 ∈ dom
(𝐴 CNF 𝐵))) ∧ 𝐶 ∈ 𝐵) → ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))) ∈
V) |
| 26 | | epelg 5585 |
. . . . . . 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 726 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ 𝐶 ∈
𝐵) → 𝐴 ∈ On) |
| 29 | | simplr 769 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ 𝐶 ∈
𝐵) → 𝐵 ∈ On) |
| 30 | | fconst6g 6797 |
. . . . . . . . . . . . . . . . . 18
⊢ (∅
∈ 𝐴 → (𝐵 × {∅}):𝐵⟶𝐴) |
| 31 | 11, 30 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ (On ∖
2o) → (𝐵
× {∅}):𝐵⟶𝐴) |
| 32 | 31 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) → (𝐵
× {∅}):𝐵⟶𝐴) |
| 33 | 4, 15 | fczfsuppd 9426 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) → (𝐵
× {∅}) finSupp ∅) |
| 34 | 1, 3, 4 | cantnfs 9706 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) → ((𝐵
× {∅}) ∈ dom (𝐴 CNF 𝐵) ↔ ((𝐵 × {∅}):𝐵⟶𝐴 ∧ (𝐵 × {∅}) finSupp
∅))) |
| 35 | 32, 33, 34 | mpbir2and 713 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) → (𝐵
× {∅}) ∈ dom (𝐴 CNF 𝐵)) |
| 36 | 35 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ 𝐶 ∈
𝐵) → (𝐵 × {∅}) ∈ dom
(𝐴 CNF 𝐵)) |
| 37 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ 𝐶 ∈
𝐵) → 𝐶 ∈ 𝐵) |
| 38 | 10 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ 𝐶 ∈
𝐵) → 1o
∈ 𝐴) |
| 39 | | fczsupp0 8218 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐵 × {∅}) supp
∅) = ∅ |
| 40 | | 0ss 4400 |
. . . . . . . . . . . . . . . 16
⊢ ∅
⊆ 𝐶 |
| 41 | 39, 40 | eqsstri 4030 |
. . . . . . . . . . . . . . 15
⊢ ((𝐵 × {∅}) supp
∅) ⊆ 𝐶 |
| 42 | 41 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ 𝐶 ∈
𝐵) → ((𝐵 × {∅}) supp
∅) ⊆ 𝐶) |
| 43 | | 0ex 5307 |
. . . . . . . . . . . . . . . . . 18
⊢ ∅
∈ V |
| 44 | 43 | fvconst2 7224 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ 𝐵 → ((𝐵 × {∅})‘𝑦) = ∅) |
| 45 | 44 | ifeq2d 4546 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ 𝐵 → if(𝑦 = 𝐶, 1o, ((𝐵 × {∅})‘𝑦)) = if(𝑦 = 𝐶, 1o, ∅)) |
| 46 | 45 | mpteq2ia 5245 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ((𝐵 × {∅})‘𝑦))) = (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) |
| 47 | 46 | eqcomi 2746 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) = (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ((𝐵 × {∅})‘𝑦))) |
| 48 | 1, 28, 29, 36, 37, 38, 42, 47 | cantnfp1 9721 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ 𝐶 ∈
𝐵) → ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) ∈ dom (𝐴 CNF 𝐵) ∧ ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))) = (((𝐴 ↑o 𝐶) ·o
1o) +o ((𝐴 CNF 𝐵)‘(𝐵 × {∅}))))) |
| 49 | 48 | simprd 495 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ 𝐶 ∈
𝐵) → ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))) = (((𝐴 ↑o 𝐶) ·o
1o) +o ((𝐴 CNF 𝐵)‘(𝐵 × {∅})))) |
| 50 | 49 | adantrl 716 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ (𝐶 ∈
On ∧ 𝐶 ∈ 𝐵)) → ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))) = (((𝐴 ↑o 𝐶) ·o
1o) +o ((𝐴 CNF 𝐵)‘(𝐵 × {∅})))) |
| 51 | | oecl 8575 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ↑o 𝐶) ∈ On) |
| 52 | 3, 51 | sylan 580 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ 𝐶 ∈
On) → (𝐴
↑o 𝐶)
∈ On) |
| 53 | | om1 8580 |
. . . . . . . . . . . . . . 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 9715 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) → ((𝐴 CNF
𝐵)‘(𝐵 × {∅})) =
∅) |
| 56 | 55 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ 𝐶 ∈
On) → ((𝐴 CNF 𝐵)‘(𝐵 × {∅})) =
∅) |
| 57 | 54, 56 | oveq12d 7449 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ 𝐶 ∈
On) → (((𝐴
↑o 𝐶)
·o 1o) +o ((𝐴 CNF 𝐵)‘(𝐵 × {∅}))) = ((𝐴 ↑o 𝐶) +o ∅)) |
| 58 | | oa0 8554 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ↑o 𝐶) ∈ On → ((𝐴 ↑o 𝐶) +o ∅) =
(𝐴 ↑o 𝐶)) |
| 59 | 52, 58 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ 𝐶 ∈
On) → ((𝐴
↑o 𝐶)
+o ∅) = (𝐴
↑o 𝐶)) |
| 60 | 57, 59 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ 𝐶 ∈
On) → (((𝐴
↑o 𝐶)
·o 1o) +o ((𝐴 CNF 𝐵)‘(𝐵 × {∅}))) = (𝐴 ↑o 𝐶)) |
| 61 | 60 | adantrr 717 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ (𝐶 ∈
On ∧ 𝐶 ∈ 𝐵)) → (((𝐴 ↑o 𝐶) ·o 1o)
+o ((𝐴 CNF 𝐵)‘(𝐵 × {∅}))) = (𝐴 ↑o 𝐶)) |
| 62 | 50, 61 | eqtrd 2777 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ (𝐶 ∈
On ∧ 𝐶 ∈ 𝐵)) → ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))) = (𝐴 ↑o 𝐶)) |
| 63 | 62 | eleq2d 2827 |
. . . . . . . . 9
⊢ (((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ (𝐶 ∈
On ∧ 𝐶 ∈ 𝐵)) → (((𝐴 CNF 𝐵)‘𝐹) ∈ ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))) ↔ ((𝐴 CNF 𝐵)‘𝐹) ∈ (𝐴 ↑o 𝐶))) |
| 64 | 63 | exp32 420 |
. . . . . . . 8
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) → (𝐶 ∈
On → (𝐶 ∈ 𝐵 → (((𝐴 CNF 𝐵)‘𝐹) ∈ ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))) ↔ ((𝐴 CNF 𝐵)‘𝐹) ∈ (𝐴 ↑o 𝐶))))) |
| 65 | 64 | adantrd 491 |
. . . . . . 7
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) → ((𝐶
∈ On ∧ 𝐹 ∈
dom (𝐴 CNF 𝐵)) → (𝐶 ∈ 𝐵 → (((𝐴 CNF 𝐵)‘𝐹) ∈ ((𝐴 CNF 𝐵)‘(𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))) ↔ ((𝐴 CNF 𝐵)‘𝐹) ∈ (𝐴 ↑o 𝐶))))) |
| 66 | 65 | imp31 417 |
. . . . . 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 6905 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝐹 → (𝑎‘𝑐) = (𝐹‘𝑐)) |
| 69 | 68 | eleq1d 2826 |
. . . . . . . . . 10
⊢ (𝑎 = 𝐹 → ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ↔ (𝐹‘𝑐) ∈ (𝑏‘𝑐))) |
| 70 | | fveq1 6905 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 𝐹 → (𝑎‘𝑥) = (𝐹‘𝑥)) |
| 71 | 70 | eqeq1d 2739 |
. . . . . . . . . . . 12
⊢ (𝑎 = 𝐹 → ((𝑎‘𝑥) = (𝑏‘𝑥) ↔ (𝐹‘𝑥) = (𝑏‘𝑥))) |
| 72 | 71 | imbi2d 340 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝐹 → ((𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥)) ↔ (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = (𝑏‘𝑥)))) |
| 73 | 72 | ralbidv 3178 |
. . . . . . . . . 10
⊢ (𝑎 = 𝐹 → (∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥)) ↔ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = (𝑏‘𝑥)))) |
| 74 | 69, 73 | anbi12d 632 |
. . . . . . . . 9
⊢ (𝑎 = 𝐹 → (((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥))) ↔ ((𝐹‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = (𝑏‘𝑥))))) |
| 75 | 74 | rexbidv 3179 |
. . . . . . . 8
⊢ (𝑎 = 𝐹 → (∃𝑐 ∈ 𝐵 ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥))) ↔ ∃𝑐 ∈ 𝐵 ((𝐹‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = (𝑏‘𝑥))))) |
| 76 | | fveq1 6905 |
. . . . . . . . . . 11
⊢ (𝑏 = (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) → (𝑏‘𝑐) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐)) |
| 77 | 76 | eleq2d 2827 |
. . . . . . . . . 10
⊢ (𝑏 = (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) → ((𝐹‘𝑐) ∈ (𝑏‘𝑐) ↔ (𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐))) |
| 78 | | fveq1 6905 |
. . . . . . . . . . . . 13
⊢ (𝑏 = (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) → (𝑏‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥)) |
| 79 | 78 | eqeq2d 2748 |
. . . . . . . . . . . 12
⊢ (𝑏 = (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) → ((𝐹‘𝑥) = (𝑏‘𝑥) ↔ (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥))) |
| 80 | 79 | imbi2d 340 |
. . . . . . . . . . 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 43336 |
. . . . . . 7
⊢ (𝐹{〈𝑎, 𝑏〉 ∣ ∃𝑐 ∈ 𝐵 ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥)))} (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) ↔ ((𝐹 ∈ V ∧ (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) ∈ V) ∧
∃𝑐 ∈ 𝐵 ((𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥))))) |
| 85 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑐 = 𝐶 → (𝐹‘𝑐) = (𝐹‘𝐶)) |
| 86 | 85 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑐 = 𝐶 ∧ 𝑐 ∈ 𝐵) → (𝐹‘𝑐) = (𝐹‘𝐶)) |
| 87 | | eqeq1 2741 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = 𝑐 → (𝑦 = 𝐶 ↔ 𝑐 = 𝐶)) |
| 88 | 87 | ifbid 4549 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = 𝑐 → if(𝑦 = 𝐶, 1o, ∅) = if(𝑐 = 𝐶, 1o, ∅)) |
| 89 | | 1oex 8516 |
. . . . . . . . . . . . . . . . . . . 20
⊢
1o ∈ V |
| 90 | 89, 43 | ifex 4576 |
. . . . . . . . . . . . . . . . . . 19
⊢ if(𝑐 = 𝐶, 1o, ∅) ∈
V |
| 91 | 88, 16, 90 | fvmpt 7016 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑐 ∈ 𝐵 → ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐) = if(𝑐 = 𝐶, 1o, ∅)) |
| 92 | | iftrue 4531 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑐 = 𝐶 → if(𝑐 = 𝐶, 1o, ∅) =
1o) |
| 93 | 91, 92 | sylan9eqr 2799 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑐 = 𝐶 ∧ 𝑐 ∈ 𝐵) → ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐) =
1o) |
| 94 | 86, 93 | eleq12d 2835 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑐 = 𝐶 ∧ 𝑐 ∈ 𝐵) → ((𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐) ↔ (𝐹‘𝐶) ∈ 1o)) |
| 95 | | el1o 8533 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹‘𝐶) ∈ 1o ↔ (𝐹‘𝐶) = ∅) |
| 96 | 95 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑐 = 𝐶 ∧ 𝑐 ∈ 𝐵) → ((𝐹‘𝐶) ∈ 1o ↔ (𝐹‘𝐶) = ∅)) |
| 97 | 96 | biimpd 229 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑐 = 𝐶 ∧ 𝑐 ∈ 𝐵) → ((𝐹‘𝐶) ∈ 1o → (𝐹‘𝐶) = ∅)) |
| 98 | | simpl 482 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑐 = 𝐶 ∧ 𝑐 ∈ 𝐵) → 𝑐 = 𝐶) |
| 99 | 97, 98 | jctild 525 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑐 = 𝐶 ∧ 𝑐 ∈ 𝐵) → ((𝐹‘𝐶) ∈ 1o → (𝑐 = 𝐶 ∧ (𝐹‘𝐶) = ∅))) |
| 100 | 94, 99 | sylbid 240 |
. . . . . . . . . . . . . . 15
⊢ ((𝑐 = 𝐶 ∧ 𝑐 ∈ 𝐵) → ((𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐) → (𝑐 = 𝐶 ∧ (𝐹‘𝐶) = ∅))) |
| 101 | 100 | expimpd 453 |
. . . . . . . . . . . . . 14
⊢ (𝑐 = 𝐶 → ((𝑐 ∈ 𝐵 ∧ (𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐)) → (𝑐 = 𝐶 ∧ (𝐹‘𝐶) = ∅))) |
| 102 | 91 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑐 ≠ 𝐶 ∧ 𝑐 ∈ 𝐵) → ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐) = if(𝑐 = 𝐶, 1o, ∅)) |
| 103 | | simpl 482 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑐 ≠ 𝐶 ∧ 𝑐 ∈ 𝐵) → 𝑐 ≠ 𝐶) |
| 104 | 103 | neneqd 2945 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑐 ≠ 𝐶 ∧ 𝑐 ∈ 𝐵) → ¬ 𝑐 = 𝐶) |
| 105 | 104 | iffalsed 4536 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑐 ≠ 𝐶 ∧ 𝑐 ∈ 𝐵) → if(𝑐 = 𝐶, 1o, ∅) =
∅) |
| 106 | 102, 105 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑐 ≠ 𝐶 ∧ 𝑐 ∈ 𝐵) → ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐) = ∅) |
| 107 | 106 | eleq2d 2827 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑐 ≠ 𝐶 ∧ 𝑐 ∈ 𝐵) → ((𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐) ↔ (𝐹‘𝑐) ∈ ∅)) |
| 108 | 107 | biimpd 229 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑐 ≠ 𝐶 ∧ 𝑐 ∈ 𝐵) → ((𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐) → (𝐹‘𝑐) ∈ ∅)) |
| 109 | 108 | expimpd 453 |
. . . . . . . . . . . . . . 15
⊢ (𝑐 ≠ 𝐶 → ((𝑐 ∈ 𝐵 ∧ (𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐)) → (𝐹‘𝑐) ∈ ∅)) |
| 110 | | noel 4338 |
. . . . . . . . . . . . . . . 16
⊢ ¬
(𝐹‘𝑐) ∈ ∅ |
| 111 | 110 | pm2.21i 119 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹‘𝑐) ∈ ∅ → (𝑐 = 𝐶 ∧ (𝐹‘𝐶) = ∅)) |
| 112 | 109, 111 | syl6 35 |
. . . . . . . . . . . . . 14
⊢ (𝑐 ≠ 𝐶 → ((𝑐 ∈ 𝐵 ∧ (𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐)) → (𝑐 = 𝐶 ∧ (𝐹‘𝐶) = ∅))) |
| 113 | 101, 112 | pm2.61ine 3025 |
. . . . . . . . . . . . 13
⊢ ((𝑐 ∈ 𝐵 ∧ (𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐)) → (𝑐 = 𝐶 ∧ (𝐹‘𝐶) = ∅)) |
| 114 | 113 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ 𝐶 ∈
On) ∧ 𝐶 ∈ 𝐵) → ((𝑐 ∈ 𝐵 ∧ (𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐)) → (𝑐 = 𝐶 ∧ (𝐹‘𝐶) = ∅))) |
| 115 | | fveqeq2 6915 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝐶 → ((𝐹‘𝑥) = ∅ ↔ (𝐹‘𝐶) = ∅)) |
| 116 | 115 | ralsng 4675 |
. . . . . . . . . . . . . . 15
⊢ (𝐶 ∈ 𝐵 → (∀𝑥 ∈ {𝐶} (𝐹‘𝑥) = ∅ ↔ (𝐹‘𝐶) = ∅)) |
| 117 | 116 | anbi2d 630 |
. . . . . . . . . . . . . 14
⊢ (𝐶 ∈ 𝐵 → ((𝑐 = 𝐶 ∧ ∀𝑥 ∈ {𝐶} (𝐹‘𝑥) = ∅) ↔ (𝑐 = 𝐶 ∧ (𝐹‘𝐶) = ∅))) |
| 118 | 117 | biimprd 248 |
. . . . . . . . . . . . 13
⊢ (𝐶 ∈ 𝐵 → ((𝑐 = 𝐶 ∧ (𝐹‘𝐶) = ∅) → (𝑐 = 𝐶 ∧ ∀𝑥 ∈ {𝐶} (𝐹‘𝑥) = ∅))) |
| 119 | 118 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ 𝐶 ∈
On) ∧ 𝐶 ∈ 𝐵) → ((𝑐 = 𝐶 ∧ (𝐹‘𝐶) = ∅) → (𝑐 = 𝐶 ∧ ∀𝑥 ∈ {𝐶} (𝐹‘𝑥) = ∅))) |
| 120 | 4 | anim1i 615 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ 𝐶 ∈
On) → (𝐵 ∈ On
∧ 𝐶 ∈
On)) |
| 121 | 120 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ 𝐶 ∈
On) ∧ 𝐶 ∈ 𝐵) → (𝐵 ∈ On ∧ 𝐶 ∈ On)) |
| 122 | | pm3.31 449 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ 𝐵 → (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥))) → ((𝑥 ∈ 𝐵 ∧ 𝑐 ∈ 𝑥) → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥))) |
| 123 | 122 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) → ((𝑥 ∈ 𝐵 → (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥))) → ((𝑥 ∈ 𝐵 ∧ 𝑐 ∈ 𝑥) → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥)))) |
| 124 | | eldif 3961 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ (𝐵 ∖ suc 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ suc 𝐶)) |
| 125 | | simplr 769 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ 𝐵) → 𝑐 = 𝐶) |
| 126 | 125 | eleq1d 2826 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ 𝐵) → (𝑐 ∈ 𝑥 ↔ 𝐶 ∈ 𝑥)) |
| 127 | | simpl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐵 ∈ On ∧ 𝐶 ∈ On) → 𝐵 ∈ On) |
| 128 | 127 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) → 𝐵 ∈ On) |
| 129 | | onelon 6409 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐵 ∈ On ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ On) |
| 130 | 128, 129 | sylan 580 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ On) |
| 131 | | simpllr 776 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ 𝐵) → 𝐶 ∈ On) |
| 132 | | ontri1 6418 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑥 ∈ On ∧ 𝐶 ∈ On) → (𝑥 ⊆ 𝐶 ↔ ¬ 𝐶 ∈ 𝑥)) |
| 133 | 130, 131,
132 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ 𝐵) → (𝑥 ⊆ 𝐶 ↔ ¬ 𝐶 ∈ 𝑥)) |
| 134 | 133 | con2bid 354 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ 𝐵) → (𝐶 ∈ 𝑥 ↔ ¬ 𝑥 ⊆ 𝐶)) |
| 135 | | onsssuc 6474 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑥 ∈ On ∧ 𝐶 ∈ On) → (𝑥 ⊆ 𝐶 ↔ 𝑥 ∈ suc 𝐶)) |
| 136 | 130, 131,
135 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . 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 579 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) → ((𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ suc 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ 𝑐 ∈ 𝑥))) |
| 140 | 124, 139 | bitrid 283 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) → (𝑥 ∈ (𝐵 ∖ suc 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ 𝑐 ∈ 𝑥))) |
| 141 | 140 | biimpd 229 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) → (𝑥 ∈ (𝐵 ∖ suc 𝐶) → (𝑥 ∈ 𝐵 ∧ 𝑐 ∈ 𝑥))) |
| 142 | 141 | imim1d 82 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) → (((𝑥 ∈ 𝐵 ∧ 𝑐 ∈ 𝑥) → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥)) → (𝑥 ∈ (𝐵 ∖ suc 𝐶) → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥)))) |
| 143 | | eldifi 4131 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 ∈ (𝐵 ∖ suc 𝐶) → 𝑥 ∈ 𝐵) |
| 144 | 143 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ (𝐵 ∖ suc 𝐶)) → 𝑥 ∈ 𝐵) |
| 145 | | eqeq1 2741 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑦 = 𝑥 → (𝑦 = 𝐶 ↔ 𝑥 = 𝐶)) |
| 146 | 145 | ifbid 4549 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦 = 𝑥 → if(𝑦 = 𝐶, 1o, ∅) = if(𝑥 = 𝐶, 1o, ∅)) |
| 147 | 89, 43 | ifex 4576 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ if(𝑥 = 𝐶, 1o, ∅) ∈
V |
| 148 | 146, 16, 147 | fvmpt 7016 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 ∈ 𝐵 → ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥) = if(𝑥 = 𝐶, 1o, ∅)) |
| 149 | 144, 148 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ (𝐵 ∖ suc 𝐶)) → ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥) = if(𝑥 = 𝐶, 1o, ∅)) |
| 150 | 128, 143,
129 | syl2an 596 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ (𝐵 ∖ suc 𝐶)) → 𝑥 ∈ On) |
| 151 | | eloni 6394 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑥 ∈ On → Ord 𝑥) |
| 152 | 150, 151 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ (𝐵 ∖ suc 𝐶)) → Ord 𝑥) |
| 153 | | eloni 6394 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝐵 ∈ On → Ord 𝐵) |
| 154 | 153 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) → Ord 𝐵) |
| 155 | | simplr 769 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) → 𝐶 ∈ On) |
| 156 | | ordeldifsucon 43272 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((Ord
𝐵 ∧ 𝐶 ∈ On) → (𝑥 ∈ (𝐵 ∖ suc 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ 𝐶 ∈ 𝑥))) |
| 157 | 154, 155,
156 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) → (𝑥 ∈ (𝐵 ∖ suc 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ 𝐶 ∈ 𝑥))) |
| 158 | 157 | biimpa 476 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ (𝐵 ∖ suc 𝐶)) → (𝑥 ∈ 𝐵 ∧ 𝐶 ∈ 𝑥)) |
| 159 | | ordirr 6402 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (Ord
𝑥 → ¬ 𝑥 ∈ 𝑥) |
| 160 | | eleq1 2829 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑥 = 𝐶 → (𝑥 ∈ 𝑥 ↔ 𝐶 ∈ 𝑥)) |
| 161 | 160 | notbid 318 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑥 = 𝐶 → (¬ 𝑥 ∈ 𝑥 ↔ ¬ 𝐶 ∈ 𝑥)) |
| 162 | 159, 161 | syl5ibcom 245 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (Ord
𝑥 → (𝑥 = 𝐶 → ¬ 𝐶 ∈ 𝑥)) |
| 163 | 162 | con2d 134 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (Ord
𝑥 → (𝐶 ∈ 𝑥 → ¬ 𝑥 = 𝐶)) |
| 164 | 163 | adantld 490 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (Ord
𝑥 → ((𝑥 ∈ 𝐵 ∧ 𝐶 ∈ 𝑥) → ¬ 𝑥 = 𝐶)) |
| 165 | 152, 158,
164 | sylc 65 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ (𝐵 ∖ suc 𝐶)) → ¬ 𝑥 = 𝐶) |
| 166 | 165 | iffalsed 4536 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ (𝐵 ∖ suc 𝐶)) → if(𝑥 = 𝐶, 1o, ∅) =
∅) |
| 167 | 149, 166 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ (𝐵 ∖ suc 𝐶)) → ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥) = ∅) |
| 168 | 167 | eqeq2d 2748 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ (𝐵 ∖ suc 𝐶)) → ((𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥) ↔ (𝐹‘𝑥) = ∅)) |
| 169 | 168 | biimpd 229 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) ∧ 𝑥 ∈ (𝐵 ∖ suc 𝐶)) → ((𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥) → (𝐹‘𝑥) = ∅)) |
| 170 | 169 | ex 412 |
. . . . . . . . . . . . . . . . . . 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 3163 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝑐 = 𝐶) → (∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥)) → ∀𝑥 ∈ (𝐵 ∖ suc 𝐶)(𝐹‘𝑥) = ∅)) |
| 174 | 121, 173 | sylan 580 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐴 ∈ (On
∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) ∧ 𝑐 = 𝐶) → (∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥)) → ∀𝑥 ∈ (𝐵 ∖ suc 𝐶)(𝐹‘𝑥) = ∅)) |
| 175 | 174 | adantr 480 |
. . . . . . . . . . . . . 14
⊢
((((((𝐴 ∈ (On
∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) ∧ 𝑐 = 𝐶) ∧ ∀𝑥 ∈ {𝐶} (𝐹‘𝑥) = ∅) → (∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥)) → ∀𝑥 ∈ (𝐵 ∖ suc 𝐶)(𝐹‘𝑥) = ∅)) |
| 176 | | ralun 4198 |
. . . . . . . . . . . . . . . . 17
⊢
((∀𝑥 ∈
{𝐶} (𝐹‘𝑥) = ∅ ∧ ∀𝑥 ∈ (𝐵 ∖ suc 𝐶)(𝐹‘𝑥) = ∅) → ∀𝑥 ∈ ({𝐶} ∪ (𝐵 ∖ suc 𝐶))(𝐹‘𝑥) = ∅) |
| 177 | 176 | adantll 714 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝐴 ∈ (On
∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) ∧ 𝑐 = 𝐶) ∧ ∀𝑥 ∈ {𝐶} (𝐹‘𝑥) = ∅) ∧ ∀𝑥 ∈ (𝐵 ∖ suc 𝐶)(𝐹‘𝑥) = ∅) → ∀𝑥 ∈ ({𝐶} ∪ (𝐵 ∖ suc 𝐶))(𝐹‘𝑥) = ∅) |
| 178 | | undif3 4300 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ({𝐶} ∪ (𝐵 ∖ suc 𝐶)) = (({𝐶} ∪ 𝐵) ∖ (suc 𝐶 ∖ {𝐶})) |
| 179 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐶 ∈ On ∧ 𝐶 ∈ 𝐵) → 𝐶 ∈ 𝐵) |
| 180 | 179 | snssd 4809 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐶 ∈ On ∧ 𝐶 ∈ 𝐵) → {𝐶} ⊆ 𝐵) |
| 181 | | ssequn1 4186 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ({𝐶} ⊆ 𝐵 ↔ ({𝐶} ∪ 𝐵) = 𝐵) |
| 182 | 180, 181 | sylib 218 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐶 ∈ On ∧ 𝐶 ∈ 𝐵) → ({𝐶} ∪ 𝐵) = 𝐵) |
| 183 | | simpl 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐶 ∈ On ∧ 𝐶 ∈ 𝐵) → 𝐶 ∈ On) |
| 184 | | eloni 6394 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐶 ∈ On → Ord 𝐶) |
| 185 | | orddif 6480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (Ord
𝐶 → 𝐶 = (suc 𝐶 ∖ {𝐶})) |
| 186 | 183, 184,
185 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐶 ∈ On ∧ 𝐶 ∈ 𝐵) → 𝐶 = (suc 𝐶 ∖ {𝐶})) |
| 187 | 186 | eqcomd 2743 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐶 ∈ On ∧ 𝐶 ∈ 𝐵) → (suc 𝐶 ∖ {𝐶}) = 𝐶) |
| 188 | 182, 187 | difeq12d 4127 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐶 ∈ On ∧ 𝐶 ∈ 𝐵) → (({𝐶} ∪ 𝐵) ∖ (suc 𝐶 ∖ {𝐶})) = (𝐵 ∖ 𝐶)) |
| 189 | 178, 188 | eqtrid 2789 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐶 ∈ On ∧ 𝐶 ∈ 𝐵) → ({𝐶} ∪ (𝐵 ∖ suc 𝐶)) = (𝐵 ∖ 𝐶)) |
| 190 | 189 | adantll 714 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ 𝐶 ∈
On) ∧ 𝐶 ∈ 𝐵) → ({𝐶} ∪ (𝐵 ∖ suc 𝐶)) = (𝐵 ∖ 𝐶)) |
| 191 | 190 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐴 ∈ (On
∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) ∧ 𝑐 = 𝐶) → ({𝐶} ∪ (𝐵 ∖ suc 𝐶)) = (𝐵 ∖ 𝐶)) |
| 192 | 191 | raleqdv 3326 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐴 ∈ (On
∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) ∧ 𝑐 = 𝐶) → (∀𝑥 ∈ ({𝐶} ∪ (𝐵 ∖ suc 𝐶))(𝐹‘𝑥) = ∅ ↔ ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅)) |
| 193 | 192 | ad2antrr 726 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝐴 ∈ (On
∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) ∧ 𝑐 = 𝐶) ∧ ∀𝑥 ∈ {𝐶} (𝐹‘𝑥) = ∅) ∧ ∀𝑥 ∈ (𝐵 ∖ suc 𝐶)(𝐹‘𝑥) = ∅) → (∀𝑥 ∈ ({𝐶} ∪ (𝐵 ∖ suc 𝐶))(𝐹‘𝑥) = ∅ ↔ ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅)) |
| 194 | 177, 193 | mpbid 232 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝐴 ∈ (On
∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) ∧ 𝑐 = 𝐶) ∧ ∀𝑥 ∈ {𝐶} (𝐹‘𝑥) = ∅) ∧ ∀𝑥 ∈ (𝐵 ∖ suc 𝐶)(𝐹‘𝑥) = ∅) → ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅) |
| 195 | 194 | ex 412 |
. . . . . . . . . . . . . 14
⊢
((((((𝐴 ∈ (On
∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) ∧ 𝑐 = 𝐶) ∧ ∀𝑥 ∈ {𝐶} (𝐹‘𝑥) = ∅) → (∀𝑥 ∈ (𝐵 ∖ suc 𝐶)(𝐹‘𝑥) = ∅ → ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅)) |
| 196 | 175, 195 | syld 47 |
. . . . . . . . . . . . 13
⊢
((((((𝐴 ∈ (On
∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) ∧ 𝑐 = 𝐶) ∧ ∀𝑥 ∈ {𝐶} (𝐹‘𝑥) = ∅) → (∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥)) → ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅)) |
| 197 | 196 | expl 457 |
. . . . . . . . . . . 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 452 |
. . . . . . . . . 10
⊢
(((((𝐴 ∈ (On
∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) → ((𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐) → (∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥)) → ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅))) |
| 200 | 199 | impd 410 |
. . . . . . . . 9
⊢
(((((𝐴 ∈ (On
∖ 2o) ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ∧ 𝐶 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) → (((𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥))) → ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅)) |
| 201 | 200 | rexlimdva 3155 |
. . . . . . . 8
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ 𝐶 ∈
On) ∧ 𝐶 ∈ 𝐵) → (∃𝑐 ∈ 𝐵 ((𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥))) → ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅)) |
| 202 | 201 | adantld 490 |
. . . . . . 7
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ 𝐶 ∈
On) ∧ 𝐶 ∈ 𝐵) → (((𝐹 ∈ V ∧ (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) ∈ V) ∧
∃𝑐 ∈ 𝐵 ((𝐹‘𝑐) ∈ ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝐹‘𝑥) = ((𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅))‘𝑥)))) → ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅)) |
| 203 | 84, 202 | biimtrid 242 |
. . . . . 6
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ 𝐶 ∈
On) ∧ 𝐶 ∈ 𝐵) → (𝐹{〈𝑎, 𝑏〉 ∣ ∃𝑐 ∈ 𝐵 ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥)))} (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) →
∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅)) |
| 204 | 203 | adantlrr 721 |
. . . . 5
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ (𝐶 ∈
On ∧ 𝐹 ∈ dom
(𝐴 CNF 𝐵))) ∧ 𝐶 ∈ 𝐵) → (𝐹{〈𝑎, 𝑏〉 ∣ ∃𝑐 ∈ 𝐵 ((𝑎‘𝑐) ∈ (𝑏‘𝑐) ∧ ∀𝑥 ∈ 𝐵 (𝑐 ∈ 𝑥 → (𝑎‘𝑥) = (𝑏‘𝑥)))} (𝑦 ∈ 𝐵 ↦ if(𝑦 = 𝐶, 1o, ∅)) →
∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅)) |
| 205 | 67, 204 | sylbid 240 |
. . . 4
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ (𝐶 ∈
On ∧ 𝐹 ∈ dom
(𝐴 CNF 𝐵))) ∧ 𝐶 ∈ 𝐵) → (((𝐴 CNF 𝐵)‘𝐹) ∈ (𝐴 ↑o 𝐶) → ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅)) |
| 206 | 205 | ex 412 |
. . 3
⊢ (((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ (𝐶 ∈
On ∧ 𝐹 ∈ dom
(𝐴 CNF 𝐵))) → (𝐶 ∈ 𝐵 → (((𝐴 CNF 𝐵)‘𝐹) ∈ (𝐴 ↑o 𝐶) → ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅))) |
| 207 | | ral0 4513 |
. . . . 5
⊢
∀𝑥 ∈
∅ (𝐹‘𝑥) = ∅ |
| 208 | | ssdif0 4366 |
. . . . . . 7
⊢ (𝐵 ⊆ 𝐶 ↔ (𝐵 ∖ 𝐶) = ∅) |
| 209 | 208 | biimpi 216 |
. . . . . 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 480 |
. . . 4
⊢ ((𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵)) → Ord 𝐶) |
| 214 | 153 | adantl 481 |
. . . 4
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) → Ord 𝐵) |
| 215 | | ordtri2or 6482 |
. . . 4
⊢ ((Ord
𝐶 ∧ Ord 𝐵) → (𝐶 ∈ 𝐵 ∨ 𝐵 ⊆ 𝐶)) |
| 216 | 213, 214,
215 | syl2anr 597 |
. . 3
⊢ (((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ (𝐶 ∈
On ∧ 𝐹 ∈ dom
(𝐴 CNF 𝐵))) → (𝐶 ∈ 𝐵 ∨ 𝐵 ⊆ 𝐶)) |
| 217 | 206, 212,
216 | mpjaod 861 |
. 2
⊢ (((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ (𝐶 ∈
On ∧ 𝐹 ∈ dom
(𝐴 CNF 𝐵))) → (((𝐴 CNF 𝐵)‘𝐹) ∈ (𝐴 ↑o 𝐶) → ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅)) |
| 218 | 3 | ad2antrr 726 |
. . . 4
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ (𝐶 ∈
On ∧ 𝐹 ∈ dom
(𝐴 CNF 𝐵))) ∧ ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅) → 𝐴 ∈ On) |
| 219 | | simpllr 776 |
. . . 4
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ (𝐶 ∈
On ∧ 𝐹 ∈ dom
(𝐴 CNF 𝐵))) ∧ ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅) → 𝐵 ∈ On) |
| 220 | | simplrr 778 |
. . . 4
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ (𝐶 ∈
On ∧ 𝐹 ∈ dom
(𝐴 CNF 𝐵))) ∧ ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅) → 𝐹 ∈ dom (𝐴 CNF 𝐵)) |
| 221 | 15 | ad2antrr 726 |
. . . 4
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ (𝐶 ∈
On ∧ 𝐹 ∈ dom
(𝐴 CNF 𝐵))) ∧ ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅) → ∅ ∈ 𝐴) |
| 222 | | simplrl 777 |
. . . 4
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ (𝐶 ∈
On ∧ 𝐹 ∈ dom
(𝐴 CNF 𝐵))) ∧ ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅) → 𝐶 ∈ On) |
| 223 | 1, 3, 4 | cantnfs 9706 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) → (𝐹 ∈
dom (𝐴 CNF 𝐵) ↔ (𝐹:𝐵⟶𝐴 ∧ 𝐹 finSupp ∅))) |
| 224 | 223 | biimpd 229 |
. . . . . . . . 9
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) → (𝐹 ∈
dom (𝐴 CNF 𝐵) → (𝐹:𝐵⟶𝐴 ∧ 𝐹 finSupp ∅))) |
| 225 | 224 | adantld 490 |
. . . . . . . 8
⊢ ((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) → ((𝐶
∈ On ∧ 𝐹 ∈
dom (𝐴 CNF 𝐵)) → (𝐹:𝐵⟶𝐴 ∧ 𝐹 finSupp ∅))) |
| 226 | 225 | imp 406 |
. . . . . . 7
⊢ (((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ (𝐶 ∈
On ∧ 𝐹 ∈ dom
(𝐴 CNF 𝐵))) → (𝐹:𝐵⟶𝐴 ∧ 𝐹 finSupp ∅)) |
| 227 | 226 | simpld 494 |
. . . . . 6
⊢ (((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ (𝐶 ∈
On ∧ 𝐹 ∈ dom
(𝐴 CNF 𝐵))) → 𝐹:𝐵⟶𝐴) |
| 228 | 227 | adantr 480 |
. . . . 5
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ (𝐶 ∈
On ∧ 𝐹 ∈ dom
(𝐴 CNF 𝐵))) ∧ ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅) → 𝐹:𝐵⟶𝐴) |
| 229 | | fveqeq2 6915 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → ((𝐹‘𝑥) = ∅ ↔ (𝐹‘𝑦) = ∅)) |
| 230 | 229 | rspccv 3619 |
. . . . . . 7
⊢
(∀𝑥 ∈
(𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅ → (𝑦 ∈ (𝐵 ∖ 𝐶) → (𝐹‘𝑦) = ∅)) |
| 231 | 230 | adantl 481 |
. . . . . 6
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ (𝐶 ∈
On ∧ 𝐹 ∈ dom
(𝐴 CNF 𝐵))) ∧ ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅) → (𝑦 ∈ (𝐵 ∖ 𝐶) → (𝐹‘𝑦) = ∅)) |
| 232 | 231 | imp 406 |
. . . . 5
⊢
(((((𝐴 ∈ (On
∖ 2o) ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐹 ∈ dom (𝐴 CNF 𝐵))) ∧ ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅) ∧ 𝑦 ∈ (𝐵 ∖ 𝐶)) → (𝐹‘𝑦) = ∅) |
| 233 | 228, 232 | suppss 8219 |
. . . 4
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ (𝐶 ∈
On ∧ 𝐹 ∈ dom
(𝐴 CNF 𝐵))) ∧ ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅) → (𝐹 supp ∅) ⊆ 𝐶) |
| 234 | 1, 218, 219, 220, 221, 222, 233 | cantnflt2 9713 |
. . 3
⊢ ((((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ (𝐶 ∈
On ∧ 𝐹 ∈ dom
(𝐴 CNF 𝐵))) ∧ ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅) → ((𝐴 CNF 𝐵)‘𝐹) ∈ (𝐴 ↑o 𝐶)) |
| 235 | 234 | ex 412 |
. 2
⊢ (((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ (𝐶 ∈
On ∧ 𝐹 ∈ dom
(𝐴 CNF 𝐵))) → (∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅ → ((𝐴 CNF 𝐵)‘𝐹) ∈ (𝐴 ↑o 𝐶))) |
| 236 | 217, 235 | impbid 212 |
1
⊢ (((𝐴 ∈ (On ∖
2o) ∧ 𝐵
∈ On) ∧ (𝐶 ∈
On ∧ 𝐹 ∈ dom
(𝐴 CNF 𝐵))) → (((𝐴 CNF 𝐵)‘𝐹) ∈ (𝐴 ↑o 𝐶) ↔ ∀𝑥 ∈ (𝐵 ∖ 𝐶)(𝐹‘𝑥) = ∅)) |