Proof of Theorem satfv1lem
| Step | Hyp | Ref
| Expression |
| 1 | | fveq1 6905 |
. . . . . . 7
⊢ (𝑏 = ({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁}))) → (𝑏‘𝐼) = (({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝐼)) |
| 2 | | fveq1 6905 |
. . . . . . 7
⊢ (𝑏 = ({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁}))) → (𝑏‘𝐽) = (({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝐽)) |
| 3 | 1, 2 | breq12d 5156 |
. . . . . 6
⊢ (𝑏 = ({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁}))) → ((𝑏‘𝐼)𝐸(𝑏‘𝐽) ↔ (({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝐼)𝐸(({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝐽))) |
| 4 | 3 | elrab 3692 |
. . . . 5
⊢
(({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁}))) ∈ {𝑏 ∈ (𝑀 ↑m ω) ∣ (𝑏‘𝐼)𝐸(𝑏‘𝐽)} ↔ (({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁}))) ∈ (𝑀 ↑m ω) ∧
(({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝐼)𝐸(({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝐽))) |
| 5 | 4 | a1i 11 |
. . . 4
⊢ ((((𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ 𝑎 ∈ (𝑀 ↑m ω)) ∧ 𝑧 ∈ 𝑀) → (({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁}))) ∈ {𝑏 ∈ (𝑀 ↑m ω) ∣ (𝑏‘𝐼)𝐸(𝑏‘𝐽)} ↔ (({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁}))) ∈ (𝑀 ↑m ω) ∧
(({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝐼)𝐸(({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝐽)))) |
| 6 | | elex 3501 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ω → 𝑁 ∈ V) |
| 7 | 6 | 3ad2ant1 1134 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω) → 𝑁 ∈ V) |
| 8 | 7 | ad2antrr 726 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ 𝑎 ∈ (𝑀 ↑m ω)) ∧ 𝑧 ∈ 𝑀) → 𝑁 ∈ V) |
| 9 | | simpr 484 |
. . . . . . . . 9
⊢ ((((𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ 𝑎 ∈ (𝑀 ↑m ω)) ∧ 𝑧 ∈ 𝑀) → 𝑧 ∈ 𝑀) |
| 10 | 8, 9 | fsnd 6891 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ 𝑎 ∈ (𝑀 ↑m ω)) ∧ 𝑧 ∈ 𝑀) → {〈𝑁, 𝑧〉}:{𝑁}⟶𝑀) |
| 11 | | elmapex 8888 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ (𝑀 ↑m ω) → (𝑀 ∈ V ∧ ω ∈
V)) |
| 12 | 11 | simpld 494 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ (𝑀 ↑m ω) → 𝑀 ∈ V) |
| 13 | 12 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝑎 ∈ (𝑀 ↑m ω) ∧ 𝑧 ∈ 𝑀) → 𝑀 ∈ V) |
| 14 | | snex 5436 |
. . . . . . . . . . 11
⊢ {𝑁} ∈ V |
| 15 | 14 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝑎 ∈ (𝑀 ↑m ω) ∧ 𝑧 ∈ 𝑀) → {𝑁} ∈ V) |
| 16 | 13, 15 | elmapd 8880 |
. . . . . . . . 9
⊢ ((𝑎 ∈ (𝑀 ↑m ω) ∧ 𝑧 ∈ 𝑀) → ({〈𝑁, 𝑧〉} ∈ (𝑀 ↑m {𝑁}) ↔ {〈𝑁, 𝑧〉}:{𝑁}⟶𝑀)) |
| 17 | 16 | adantll 714 |
. . . . . . . 8
⊢ ((((𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ 𝑎 ∈ (𝑀 ↑m ω)) ∧ 𝑧 ∈ 𝑀) → ({〈𝑁, 𝑧〉} ∈ (𝑀 ↑m {𝑁}) ↔ {〈𝑁, 𝑧〉}:{𝑁}⟶𝑀)) |
| 18 | 10, 17 | mpbird 257 |
. . . . . . 7
⊢ ((((𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ 𝑎 ∈ (𝑀 ↑m ω)) ∧ 𝑧 ∈ 𝑀) → {〈𝑁, 𝑧〉} ∈ (𝑀 ↑m {𝑁})) |
| 19 | | elmapi 8889 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ (𝑀 ↑m ω) → 𝑎:ω⟶𝑀) |
| 20 | | difssd 4137 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ (𝑀 ↑m ω) → (ω
∖ {𝑁}) ⊆
ω) |
| 21 | 19, 20 | fssresd 6775 |
. . . . . . . . . 10
⊢ (𝑎 ∈ (𝑀 ↑m ω) → (𝑎 ↾ (ω ∖ {𝑁})):(ω ∖ {𝑁})⟶𝑀) |
| 22 | | omex 9683 |
. . . . . . . . . . . . 13
⊢ ω
∈ V |
| 23 | 22 | difexi 5330 |
. . . . . . . . . . . 12
⊢ (ω
∖ {𝑁}) ∈
V |
| 24 | 23 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ (𝑀 ↑m ω) → (ω
∖ {𝑁}) ∈
V) |
| 25 | 12, 24 | elmapd 8880 |
. . . . . . . . . 10
⊢ (𝑎 ∈ (𝑀 ↑m ω) → ((𝑎 ↾ (ω ∖ {𝑁})) ∈ (𝑀 ↑m (ω ∖ {𝑁})) ↔ (𝑎 ↾ (ω ∖ {𝑁})):(ω ∖ {𝑁})⟶𝑀)) |
| 26 | 21, 25 | mpbird 257 |
. . . . . . . . 9
⊢ (𝑎 ∈ (𝑀 ↑m ω) → (𝑎 ↾ (ω ∖ {𝑁})) ∈ (𝑀 ↑m (ω ∖ {𝑁}))) |
| 27 | 26 | adantl 481 |
. . . . . . . 8
⊢ (((𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ 𝑎 ∈ (𝑀 ↑m ω)) → (𝑎 ↾ (ω ∖ {𝑁})) ∈ (𝑀 ↑m (ω ∖ {𝑁}))) |
| 28 | 27 | adantr 480 |
. . . . . . 7
⊢ ((((𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ 𝑎 ∈ (𝑀 ↑m ω)) ∧ 𝑧 ∈ 𝑀) → (𝑎 ↾ (ω ∖ {𝑁})) ∈ (𝑀 ↑m (ω ∖ {𝑁}))) |
| 29 | | res0 6001 |
. . . . . . . . . 10
⊢
({〈𝑁, 𝑧〉} ↾ ∅) =
∅ |
| 30 | | res0 6001 |
. . . . . . . . . 10
⊢ ((𝑎 ↾ (ω ∖ {𝑁})) ↾ ∅) =
∅ |
| 31 | 29, 30 | eqtr4i 2768 |
. . . . . . . . 9
⊢
({〈𝑁, 𝑧〉} ↾ ∅) =
((𝑎 ↾ (ω
∖ {𝑁})) ↾
∅) |
| 32 | | disjdif 4472 |
. . . . . . . . . 10
⊢ ({𝑁} ∩ (ω ∖ {𝑁})) = ∅ |
| 33 | 32 | reseq2i 5994 |
. . . . . . . . 9
⊢
({〈𝑁, 𝑧〉} ↾ ({𝑁} ∩ (ω ∖ {𝑁}))) = ({〈𝑁, 𝑧〉} ↾ ∅) |
| 34 | 32 | reseq2i 5994 |
. . . . . . . . 9
⊢ ((𝑎 ↾ (ω ∖ {𝑁})) ↾ ({𝑁} ∩ (ω ∖ {𝑁}))) = ((𝑎 ↾ (ω ∖ {𝑁})) ↾ ∅) |
| 35 | 31, 33, 34 | 3eqtr4i 2775 |
. . . . . . . 8
⊢
({〈𝑁, 𝑧〉} ↾ ({𝑁} ∩ (ω ∖ {𝑁}))) = ((𝑎 ↾ (ω ∖ {𝑁})) ↾ ({𝑁} ∩ (ω ∖ {𝑁}))) |
| 36 | 35 | a1i 11 |
. . . . . . 7
⊢ ((((𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ 𝑎 ∈ (𝑀 ↑m ω)) ∧ 𝑧 ∈ 𝑀) → ({〈𝑁, 𝑧〉} ↾ ({𝑁} ∩ (ω ∖ {𝑁}))) = ((𝑎 ↾ (ω ∖ {𝑁})) ↾ ({𝑁} ∩ (ω ∖ {𝑁})))) |
| 37 | | elmapresaun 8920 |
. . . . . . 7
⊢
(({〈𝑁, 𝑧〉} ∈ (𝑀 ↑m {𝑁}) ∧ (𝑎 ↾ (ω ∖ {𝑁})) ∈ (𝑀 ↑m (ω ∖ {𝑁})) ∧ ({〈𝑁, 𝑧〉} ↾ ({𝑁} ∩ (ω ∖ {𝑁}))) = ((𝑎 ↾ (ω ∖ {𝑁})) ↾ ({𝑁} ∩ (ω ∖ {𝑁})))) → ({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁}))) ∈ (𝑀 ↑m ({𝑁} ∪ (ω ∖ {𝑁})))) |
| 38 | 18, 28, 36, 37 | syl3anc 1373 |
. . . . . 6
⊢ ((((𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ 𝑎 ∈ (𝑀 ↑m ω)) ∧ 𝑧 ∈ 𝑀) → ({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁}))) ∈ (𝑀 ↑m ({𝑁} ∪ (ω ∖ {𝑁})))) |
| 39 | | uncom 4158 |
. . . . . . . . . 10
⊢ ({𝑁} ∪ (ω ∖ {𝑁})) = ((ω ∖ {𝑁}) ∪ {𝑁}) |
| 40 | | difsnid 4810 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ω → ((ω
∖ {𝑁}) ∪ {𝑁}) = ω) |
| 41 | 39, 40 | eqtr2id 2790 |
. . . . . . . . 9
⊢ (𝑁 ∈ ω → ω =
({𝑁} ∪ (ω ∖
{𝑁}))) |
| 42 | 41 | 3ad2ant1 1134 |
. . . . . . . 8
⊢ ((𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω) → ω
= ({𝑁} ∪ (ω
∖ {𝑁}))) |
| 43 | 42 | ad2antrr 726 |
. . . . . . 7
⊢ ((((𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ 𝑎 ∈ (𝑀 ↑m ω)) ∧ 𝑧 ∈ 𝑀) → ω = ({𝑁} ∪ (ω ∖ {𝑁}))) |
| 44 | 43 | oveq2d 7447 |
. . . . . 6
⊢ ((((𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ 𝑎 ∈ (𝑀 ↑m ω)) ∧ 𝑧 ∈ 𝑀) → (𝑀 ↑m ω) = (𝑀 ↑m ({𝑁} ∪ (ω ∖ {𝑁})))) |
| 45 | 38, 44 | eleqtrrd 2844 |
. . . . 5
⊢ ((((𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ 𝑎 ∈ (𝑀 ↑m ω)) ∧ 𝑧 ∈ 𝑀) → ({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁}))) ∈ (𝑀 ↑m
ω)) |
| 46 | | ibar 528 |
. . . . . . . 8
⊢
(({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁}))) ∈ (𝑀 ↑m ω) →
((({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝐼)𝐸(({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝐽) ↔ (({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁}))) ∈ (𝑀 ↑m ω) ∧
(({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝐼)𝐸(({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝐽)))) |
| 47 | 46 | adantl 481 |
. . . . . . 7
⊢
(((((𝑁 ∈
ω ∧ 𝐼 ∈
ω ∧ 𝐽 ∈
ω) ∧ 𝑎 ∈
(𝑀 ↑m
ω)) ∧ 𝑧 ∈
𝑀) ∧ ({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁}))) ∈ (𝑀 ↑m ω)) →
((({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝐼)𝐸(({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝐽) ↔ (({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁}))) ∈ (𝑀 ↑m ω) ∧
(({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝐼)𝐸(({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝐽)))) |
| 48 | 47 | bicomd 223 |
. . . . . 6
⊢
(((((𝑁 ∈
ω ∧ 𝐼 ∈
ω ∧ 𝐽 ∈
ω) ∧ 𝑎 ∈
(𝑀 ↑m
ω)) ∧ 𝑧 ∈
𝑀) ∧ ({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁}))) ∈ (𝑀 ↑m ω)) →
((({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁}))) ∈ (𝑀 ↑m ω) ∧
(({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝐼)𝐸(({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝐽)) ↔ (({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝐼)𝐸(({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝐽))) |
| 49 | | simpll1 1213 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ 𝑎 ∈ (𝑀 ↑m ω)) ∧ 𝑧 ∈ 𝑀) → 𝑁 ∈ ω) |
| 50 | | eqid 2737 |
. . . . . . . . . . . . . . 15
⊢
({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁}))) = ({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁}))) |
| 51 | 49, 9, 50 | fvsnun1 7202 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ 𝑎 ∈ (𝑀 ↑m ω)) ∧ 𝑧 ∈ 𝑀) → (({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝑁) = 𝑧) |
| 52 | 51 | adantr 480 |
. . . . . . . . . . . . 13
⊢
(((((𝑁 ∈
ω ∧ 𝐼 ∈
ω ∧ 𝐽 ∈
ω) ∧ 𝑎 ∈
(𝑀 ↑m
ω)) ∧ 𝑧 ∈
𝑀) ∧ ({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁}))) ∈ (𝑀 ↑m ω)) →
(({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝑁) = 𝑧) |
| 53 | 52, 52 | breq12d 5156 |
. . . . . . . . . . . 12
⊢
(((((𝑁 ∈
ω ∧ 𝐼 ∈
ω ∧ 𝐽 ∈
ω) ∧ 𝑎 ∈
(𝑀 ↑m
ω)) ∧ 𝑧 ∈
𝑀) ∧ ({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁}))) ∈ (𝑀 ↑m ω)) →
((({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝑁)𝐸(({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝑁) ↔ 𝑧𝐸𝑧)) |
| 54 | 53 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝐽 = 𝑁 ∧ ((((𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ 𝑎 ∈ (𝑀 ↑m ω)) ∧ 𝑧 ∈ 𝑀) ∧ ({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁}))) ∈ (𝑀 ↑m ω))) →
((({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝑁)𝐸(({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝑁) ↔ 𝑧𝐸𝑧)) |
| 55 | | fveq2 6906 |
. . . . . . . . . . . . . 14
⊢ (𝐽 = 𝑁 → (({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝐽) = (({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝑁)) |
| 56 | 55 | breq2d 5155 |
. . . . . . . . . . . . 13
⊢ (𝐽 = 𝑁 → ((({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝑁)𝐸(({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝐽) ↔ (({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝑁)𝐸(({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝑁))) |
| 57 | | ifptru 1075 |
. . . . . . . . . . . . 13
⊢ (𝐽 = 𝑁 → (if-(𝐽 = 𝑁, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝐽)) ↔ 𝑧𝐸𝑧)) |
| 58 | 56, 57 | bibi12d 345 |
. . . . . . . . . . . 12
⊢ (𝐽 = 𝑁 → (((({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝑁)𝐸(({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝐽) ↔ if-(𝐽 = 𝑁, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝐽))) ↔ ((({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝑁)𝐸(({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝑁) ↔ 𝑧𝐸𝑧))) |
| 59 | 58 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝐽 = 𝑁 ∧ ((((𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ 𝑎 ∈ (𝑀 ↑m ω)) ∧ 𝑧 ∈ 𝑀) ∧ ({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁}))) ∈ (𝑀 ↑m ω))) →
(((({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝑁)𝐸(({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝐽) ↔ if-(𝐽 = 𝑁, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝐽))) ↔ ((({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝑁)𝐸(({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝑁) ↔ 𝑧𝐸𝑧))) |
| 60 | 54, 59 | mpbird 257 |
. . . . . . . . . 10
⊢ ((𝐽 = 𝑁 ∧ ((((𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ 𝑎 ∈ (𝑀 ↑m ω)) ∧ 𝑧 ∈ 𝑀) ∧ ({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁}))) ∈ (𝑀 ↑m ω))) →
((({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝑁)𝐸(({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝐽) ↔ if-(𝐽 = 𝑁, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝐽)))) |
| 61 | 52 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((¬
𝐽 = 𝑁 ∧ ((((𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ 𝑎 ∈ (𝑀 ↑m ω)) ∧ 𝑧 ∈ 𝑀) ∧ ({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁}))) ∈ (𝑀 ↑m ω))) →
(({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝑁) = 𝑧) |
| 62 | 49 | adantr 480 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈
ω ∧ 𝐼 ∈
ω ∧ 𝐽 ∈
ω) ∧ 𝑎 ∈
(𝑀 ↑m
ω)) ∧ 𝑧 ∈
𝑀) ∧ ({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁}))) ∈ (𝑀 ↑m ω)) → 𝑁 ∈
ω) |
| 63 | 62 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((¬
𝐽 = 𝑁 ∧ ((((𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ 𝑎 ∈ (𝑀 ↑m ω)) ∧ 𝑧 ∈ 𝑀) ∧ ({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁}))) ∈ (𝑀 ↑m ω))) → 𝑁 ∈
ω) |
| 64 | 9 | adantr 480 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈
ω ∧ 𝐼 ∈
ω ∧ 𝐽 ∈
ω) ∧ 𝑎 ∈
(𝑀 ↑m
ω)) ∧ 𝑧 ∈
𝑀) ∧ ({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁}))) ∈ (𝑀 ↑m ω)) → 𝑧 ∈ 𝑀) |
| 65 | 64 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((¬
𝐽 = 𝑁 ∧ ((((𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ 𝑎 ∈ (𝑀 ↑m ω)) ∧ 𝑧 ∈ 𝑀) ∧ ({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁}))) ∈ (𝑀 ↑m ω))) → 𝑧 ∈ 𝑀) |
| 66 | | neqne 2948 |
. . . . . . . . . . . . . . 15
⊢ (¬
𝐽 = 𝑁 → 𝐽 ≠ 𝑁) |
| 67 | | simpll3 1215 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ 𝑎 ∈ (𝑀 ↑m ω)) ∧ 𝑧 ∈ 𝑀) → 𝐽 ∈ ω) |
| 68 | 67 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑁 ∈
ω ∧ 𝐼 ∈
ω ∧ 𝐽 ∈
ω) ∧ 𝑎 ∈
(𝑀 ↑m
ω)) ∧ 𝑧 ∈
𝑀) ∧ ({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁}))) ∈ (𝑀 ↑m ω)) → 𝐽 ∈
ω) |
| 69 | 66, 68 | anim12ci 614 |
. . . . . . . . . . . . . 14
⊢ ((¬
𝐽 = 𝑁 ∧ ((((𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ 𝑎 ∈ (𝑀 ↑m ω)) ∧ 𝑧 ∈ 𝑀) ∧ ({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁}))) ∈ (𝑀 ↑m ω))) → (𝐽 ∈ ω ∧ 𝐽 ≠ 𝑁)) |
| 70 | | eldifsn 4786 |
. . . . . . . . . . . . . 14
⊢ (𝐽 ∈ (ω ∖ {𝑁}) ↔ (𝐽 ∈ ω ∧ 𝐽 ≠ 𝑁)) |
| 71 | 69, 70 | sylibr 234 |
. . . . . . . . . . . . 13
⊢ ((¬
𝐽 = 𝑁 ∧ ((((𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ 𝑎 ∈ (𝑀 ↑m ω)) ∧ 𝑧 ∈ 𝑀) ∧ ({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁}))) ∈ (𝑀 ↑m ω))) → 𝐽 ∈ (ω ∖ {𝑁})) |
| 72 | 63, 65, 50, 71 | fvsnun2 7203 |
. . . . . . . . . . . 12
⊢ ((¬
𝐽 = 𝑁 ∧ ((((𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ 𝑎 ∈ (𝑀 ↑m ω)) ∧ 𝑧 ∈ 𝑀) ∧ ({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁}))) ∈ (𝑀 ↑m ω))) →
(({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝐽) = (𝑎‘𝐽)) |
| 73 | 61, 72 | breq12d 5156 |
. . . . . . . . . . 11
⊢ ((¬
𝐽 = 𝑁 ∧ ((((𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ 𝑎 ∈ (𝑀 ↑m ω)) ∧ 𝑧 ∈ 𝑀) ∧ ({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁}))) ∈ (𝑀 ↑m ω))) →
((({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝑁)𝐸(({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝐽) ↔ 𝑧𝐸(𝑎‘𝐽))) |
| 74 | | ifpfal 1076 |
. . . . . . . . . . . . 13
⊢ (¬
𝐽 = 𝑁 → (if-(𝐽 = 𝑁, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝐽)) ↔ 𝑧𝐸(𝑎‘𝐽))) |
| 75 | 74 | bicomd 223 |
. . . . . . . . . . . 12
⊢ (¬
𝐽 = 𝑁 → (𝑧𝐸(𝑎‘𝐽) ↔ if-(𝐽 = 𝑁, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝐽)))) |
| 76 | 75 | adantr 480 |
. . . . . . . . . . 11
⊢ ((¬
𝐽 = 𝑁 ∧ ((((𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ 𝑎 ∈ (𝑀 ↑m ω)) ∧ 𝑧 ∈ 𝑀) ∧ ({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁}))) ∈ (𝑀 ↑m ω))) → (𝑧𝐸(𝑎‘𝐽) ↔ if-(𝐽 = 𝑁, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝐽)))) |
| 77 | 73, 76 | bitrd 279 |
. . . . . . . . . 10
⊢ ((¬
𝐽 = 𝑁 ∧ ((((𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ 𝑎 ∈ (𝑀 ↑m ω)) ∧ 𝑧 ∈ 𝑀) ∧ ({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁}))) ∈ (𝑀 ↑m ω))) →
((({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝑁)𝐸(({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝐽) ↔ if-(𝐽 = 𝑁, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝐽)))) |
| 78 | 60, 77 | pm2.61ian 812 |
. . . . . . . . 9
⊢
(((((𝑁 ∈
ω ∧ 𝐼 ∈
ω ∧ 𝐽 ∈
ω) ∧ 𝑎 ∈
(𝑀 ↑m
ω)) ∧ 𝑧 ∈
𝑀) ∧ ({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁}))) ∈ (𝑀 ↑m ω)) →
((({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝑁)𝐸(({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝐽) ↔ if-(𝐽 = 𝑁, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝐽)))) |
| 79 | 78 | adantl 481 |
. . . . . . . 8
⊢ ((𝐼 = 𝑁 ∧ ((((𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ 𝑎 ∈ (𝑀 ↑m ω)) ∧ 𝑧 ∈ 𝑀) ∧ ({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁}))) ∈ (𝑀 ↑m ω))) →
((({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝑁)𝐸(({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝐽) ↔ if-(𝐽 = 𝑁, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝐽)))) |
| 80 | | fveq2 6906 |
. . . . . . . . . . 11
⊢ (𝐼 = 𝑁 → (({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝐼) = (({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝑁)) |
| 81 | 80 | breq1d 5153 |
. . . . . . . . . 10
⊢ (𝐼 = 𝑁 → ((({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝐼)𝐸(({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝐽) ↔ (({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝑁)𝐸(({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝐽))) |
| 82 | | ifptru 1075 |
. . . . . . . . . 10
⊢ (𝐼 = 𝑁 → (if-(𝐼 = 𝑁, if-(𝐽 = 𝑁, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝐽)), if-(𝐽 = 𝑁, (𝑎‘𝐼)𝐸𝑧, (𝑎‘𝐼)𝐸(𝑎‘𝐽))) ↔ if-(𝐽 = 𝑁, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝐽)))) |
| 83 | 81, 82 | bibi12d 345 |
. . . . . . . . 9
⊢ (𝐼 = 𝑁 → (((({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝐼)𝐸(({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝐽) ↔ if-(𝐼 = 𝑁, if-(𝐽 = 𝑁, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝐽)), if-(𝐽 = 𝑁, (𝑎‘𝐼)𝐸𝑧, (𝑎‘𝐼)𝐸(𝑎‘𝐽)))) ↔ ((({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝑁)𝐸(({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝐽) ↔ if-(𝐽 = 𝑁, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝐽))))) |
| 84 | 83 | adantr 480 |
. . . . . . . 8
⊢ ((𝐼 = 𝑁 ∧ ((((𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ 𝑎 ∈ (𝑀 ↑m ω)) ∧ 𝑧 ∈ 𝑀) ∧ ({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁}))) ∈ (𝑀 ↑m ω))) →
(((({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝐼)𝐸(({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝐽) ↔ if-(𝐼 = 𝑁, if-(𝐽 = 𝑁, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝐽)), if-(𝐽 = 𝑁, (𝑎‘𝐼)𝐸𝑧, (𝑎‘𝐼)𝐸(𝑎‘𝐽)))) ↔ ((({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝑁)𝐸(({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝐽) ↔ if-(𝐽 = 𝑁, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝐽))))) |
| 85 | 79, 84 | mpbird 257 |
. . . . . . 7
⊢ ((𝐼 = 𝑁 ∧ ((((𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ 𝑎 ∈ (𝑀 ↑m ω)) ∧ 𝑧 ∈ 𝑀) ∧ ({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁}))) ∈ (𝑀 ↑m ω))) →
((({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝐼)𝐸(({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝐽) ↔ if-(𝐼 = 𝑁, if-(𝐽 = 𝑁, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝐽)), if-(𝐽 = 𝑁, (𝑎‘𝐼)𝐸𝑧, (𝑎‘𝐼)𝐸(𝑎‘𝐽))))) |
| 86 | 62 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((¬
𝐼 = 𝑁 ∧ ((((𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ 𝑎 ∈ (𝑀 ↑m ω)) ∧ 𝑧 ∈ 𝑀) ∧ ({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁}))) ∈ (𝑀 ↑m ω))) → 𝑁 ∈
ω) |
| 87 | 64 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((¬
𝐼 = 𝑁 ∧ ((((𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ 𝑎 ∈ (𝑀 ↑m ω)) ∧ 𝑧 ∈ 𝑀) ∧ ({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁}))) ∈ (𝑀 ↑m ω))) → 𝑧 ∈ 𝑀) |
| 88 | | neqne 2948 |
. . . . . . . . . . . . . . 15
⊢ (¬
𝐼 = 𝑁 → 𝐼 ≠ 𝑁) |
| 89 | | simpll2 1214 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ 𝑎 ∈ (𝑀 ↑m ω)) ∧ 𝑧 ∈ 𝑀) → 𝐼 ∈ ω) |
| 90 | 89 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑁 ∈
ω ∧ 𝐼 ∈
ω ∧ 𝐽 ∈
ω) ∧ 𝑎 ∈
(𝑀 ↑m
ω)) ∧ 𝑧 ∈
𝑀) ∧ ({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁}))) ∈ (𝑀 ↑m ω)) → 𝐼 ∈
ω) |
| 91 | 88, 90 | anim12ci 614 |
. . . . . . . . . . . . . 14
⊢ ((¬
𝐼 = 𝑁 ∧ ((((𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ 𝑎 ∈ (𝑀 ↑m ω)) ∧ 𝑧 ∈ 𝑀) ∧ ({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁}))) ∈ (𝑀 ↑m ω))) → (𝐼 ∈ ω ∧ 𝐼 ≠ 𝑁)) |
| 92 | | eldifsn 4786 |
. . . . . . . . . . . . . 14
⊢ (𝐼 ∈ (ω ∖ {𝑁}) ↔ (𝐼 ∈ ω ∧ 𝐼 ≠ 𝑁)) |
| 93 | 91, 92 | sylibr 234 |
. . . . . . . . . . . . 13
⊢ ((¬
𝐼 = 𝑁 ∧ ((((𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ 𝑎 ∈ (𝑀 ↑m ω)) ∧ 𝑧 ∈ 𝑀) ∧ ({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁}))) ∈ (𝑀 ↑m ω))) → 𝐼 ∈ (ω ∖ {𝑁})) |
| 94 | 86, 87, 50, 93 | fvsnun2 7203 |
. . . . . . . . . . . 12
⊢ ((¬
𝐼 = 𝑁 ∧ ((((𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ 𝑎 ∈ (𝑀 ↑m ω)) ∧ 𝑧 ∈ 𝑀) ∧ ({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁}))) ∈ (𝑀 ↑m ω))) →
(({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝐼) = (𝑎‘𝐼)) |
| 95 | 52 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((¬
𝐼 = 𝑁 ∧ ((((𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ 𝑎 ∈ (𝑀 ↑m ω)) ∧ 𝑧 ∈ 𝑀) ∧ ({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁}))) ∈ (𝑀 ↑m ω))) →
(({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝑁) = 𝑧) |
| 96 | 94, 95 | breq12d 5156 |
. . . . . . . . . . 11
⊢ ((¬
𝐼 = 𝑁 ∧ ((((𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ 𝑎 ∈ (𝑀 ↑m ω)) ∧ 𝑧 ∈ 𝑀) ∧ ({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁}))) ∈ (𝑀 ↑m ω))) →
((({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝐼)𝐸(({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝑁) ↔ (𝑎‘𝐼)𝐸𝑧)) |
| 97 | 96 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝐽 = 𝑁 ∧ (¬ 𝐼 = 𝑁 ∧ ((((𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ 𝑎 ∈ (𝑀 ↑m ω)) ∧ 𝑧 ∈ 𝑀) ∧ ({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁}))) ∈ (𝑀 ↑m ω)))) →
((({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝐼)𝐸(({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝑁) ↔ (𝑎‘𝐼)𝐸𝑧)) |
| 98 | 55 | breq2d 5155 |
. . . . . . . . . . . 12
⊢ (𝐽 = 𝑁 → ((({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝐼)𝐸(({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝐽) ↔ (({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝐼)𝐸(({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝑁))) |
| 99 | | ifptru 1075 |
. . . . . . . . . . . 12
⊢ (𝐽 = 𝑁 → (if-(𝐽 = 𝑁, (𝑎‘𝐼)𝐸𝑧, (𝑎‘𝐼)𝐸(𝑎‘𝐽)) ↔ (𝑎‘𝐼)𝐸𝑧)) |
| 100 | 98, 99 | bibi12d 345 |
. . . . . . . . . . 11
⊢ (𝐽 = 𝑁 → (((({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝐼)𝐸(({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝐽) ↔ if-(𝐽 = 𝑁, (𝑎‘𝐼)𝐸𝑧, (𝑎‘𝐼)𝐸(𝑎‘𝐽))) ↔ ((({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝐼)𝐸(({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝑁) ↔ (𝑎‘𝐼)𝐸𝑧))) |
| 101 | 100 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝐽 = 𝑁 ∧ (¬ 𝐼 = 𝑁 ∧ ((((𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ 𝑎 ∈ (𝑀 ↑m ω)) ∧ 𝑧 ∈ 𝑀) ∧ ({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁}))) ∈ (𝑀 ↑m ω)))) →
(((({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝐼)𝐸(({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝐽) ↔ if-(𝐽 = 𝑁, (𝑎‘𝐼)𝐸𝑧, (𝑎‘𝐼)𝐸(𝑎‘𝐽))) ↔ ((({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝐼)𝐸(({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝑁) ↔ (𝑎‘𝐼)𝐸𝑧))) |
| 102 | 97, 101 | mpbird 257 |
. . . . . . . . 9
⊢ ((𝐽 = 𝑁 ∧ (¬ 𝐼 = 𝑁 ∧ ((((𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ 𝑎 ∈ (𝑀 ↑m ω)) ∧ 𝑧 ∈ 𝑀) ∧ ({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁}))) ∈ (𝑀 ↑m ω)))) →
((({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝐼)𝐸(({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝐽) ↔ if-(𝐽 = 𝑁, (𝑎‘𝐼)𝐸𝑧, (𝑎‘𝐼)𝐸(𝑎‘𝐽)))) |
| 103 | 94 | adantl 481 |
. . . . . . . . . . 11
⊢ ((¬
𝐽 = 𝑁 ∧ (¬ 𝐼 = 𝑁 ∧ ((((𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ 𝑎 ∈ (𝑀 ↑m ω)) ∧ 𝑧 ∈ 𝑀) ∧ ({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁}))) ∈ (𝑀 ↑m ω)))) →
(({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝐼) = (𝑎‘𝐼)) |
| 104 | 72 | adantrl 716 |
. . . . . . . . . . 11
⊢ ((¬
𝐽 = 𝑁 ∧ (¬ 𝐼 = 𝑁 ∧ ((((𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ 𝑎 ∈ (𝑀 ↑m ω)) ∧ 𝑧 ∈ 𝑀) ∧ ({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁}))) ∈ (𝑀 ↑m ω)))) →
(({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝐽) = (𝑎‘𝐽)) |
| 105 | 103, 104 | breq12d 5156 |
. . . . . . . . . 10
⊢ ((¬
𝐽 = 𝑁 ∧ (¬ 𝐼 = 𝑁 ∧ ((((𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ 𝑎 ∈ (𝑀 ↑m ω)) ∧ 𝑧 ∈ 𝑀) ∧ ({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁}))) ∈ (𝑀 ↑m ω)))) →
((({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝐼)𝐸(({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝐽) ↔ (𝑎‘𝐼)𝐸(𝑎‘𝐽))) |
| 106 | | ifpfal 1076 |
. . . . . . . . . . . 12
⊢ (¬
𝐽 = 𝑁 → (if-(𝐽 = 𝑁, (𝑎‘𝐼)𝐸𝑧, (𝑎‘𝐼)𝐸(𝑎‘𝐽)) ↔ (𝑎‘𝐼)𝐸(𝑎‘𝐽))) |
| 107 | 106 | bicomd 223 |
. . . . . . . . . . 11
⊢ (¬
𝐽 = 𝑁 → ((𝑎‘𝐼)𝐸(𝑎‘𝐽) ↔ if-(𝐽 = 𝑁, (𝑎‘𝐼)𝐸𝑧, (𝑎‘𝐼)𝐸(𝑎‘𝐽)))) |
| 108 | 107 | adantr 480 |
. . . . . . . . . 10
⊢ ((¬
𝐽 = 𝑁 ∧ (¬ 𝐼 = 𝑁 ∧ ((((𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ 𝑎 ∈ (𝑀 ↑m ω)) ∧ 𝑧 ∈ 𝑀) ∧ ({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁}))) ∈ (𝑀 ↑m ω)))) →
((𝑎‘𝐼)𝐸(𝑎‘𝐽) ↔ if-(𝐽 = 𝑁, (𝑎‘𝐼)𝐸𝑧, (𝑎‘𝐼)𝐸(𝑎‘𝐽)))) |
| 109 | 105, 108 | bitrd 279 |
. . . . . . . . 9
⊢ ((¬
𝐽 = 𝑁 ∧ (¬ 𝐼 = 𝑁 ∧ ((((𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ 𝑎 ∈ (𝑀 ↑m ω)) ∧ 𝑧 ∈ 𝑀) ∧ ({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁}))) ∈ (𝑀 ↑m ω)))) →
((({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝐼)𝐸(({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝐽) ↔ if-(𝐽 = 𝑁, (𝑎‘𝐼)𝐸𝑧, (𝑎‘𝐼)𝐸(𝑎‘𝐽)))) |
| 110 | 102, 109 | pm2.61ian 812 |
. . . . . . . 8
⊢ ((¬
𝐼 = 𝑁 ∧ ((((𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ 𝑎 ∈ (𝑀 ↑m ω)) ∧ 𝑧 ∈ 𝑀) ∧ ({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁}))) ∈ (𝑀 ↑m ω))) →
((({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝐼)𝐸(({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝐽) ↔ if-(𝐽 = 𝑁, (𝑎‘𝐼)𝐸𝑧, (𝑎‘𝐼)𝐸(𝑎‘𝐽)))) |
| 111 | | ifpfal 1076 |
. . . . . . . . . 10
⊢ (¬
𝐼 = 𝑁 → (if-(𝐼 = 𝑁, if-(𝐽 = 𝑁, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝐽)), if-(𝐽 = 𝑁, (𝑎‘𝐼)𝐸𝑧, (𝑎‘𝐼)𝐸(𝑎‘𝐽))) ↔ if-(𝐽 = 𝑁, (𝑎‘𝐼)𝐸𝑧, (𝑎‘𝐼)𝐸(𝑎‘𝐽)))) |
| 112 | 111 | bicomd 223 |
. . . . . . . . 9
⊢ (¬
𝐼 = 𝑁 → (if-(𝐽 = 𝑁, (𝑎‘𝐼)𝐸𝑧, (𝑎‘𝐼)𝐸(𝑎‘𝐽)) ↔ if-(𝐼 = 𝑁, if-(𝐽 = 𝑁, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝐽)), if-(𝐽 = 𝑁, (𝑎‘𝐼)𝐸𝑧, (𝑎‘𝐼)𝐸(𝑎‘𝐽))))) |
| 113 | 112 | adantr 480 |
. . . . . . . 8
⊢ ((¬
𝐼 = 𝑁 ∧ ((((𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ 𝑎 ∈ (𝑀 ↑m ω)) ∧ 𝑧 ∈ 𝑀) ∧ ({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁}))) ∈ (𝑀 ↑m ω))) →
(if-(𝐽 = 𝑁, (𝑎‘𝐼)𝐸𝑧, (𝑎‘𝐼)𝐸(𝑎‘𝐽)) ↔ if-(𝐼 = 𝑁, if-(𝐽 = 𝑁, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝐽)), if-(𝐽 = 𝑁, (𝑎‘𝐼)𝐸𝑧, (𝑎‘𝐼)𝐸(𝑎‘𝐽))))) |
| 114 | 110, 113 | bitrd 279 |
. . . . . . 7
⊢ ((¬
𝐼 = 𝑁 ∧ ((((𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ 𝑎 ∈ (𝑀 ↑m ω)) ∧ 𝑧 ∈ 𝑀) ∧ ({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁}))) ∈ (𝑀 ↑m ω))) →
((({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝐼)𝐸(({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝐽) ↔ if-(𝐼 = 𝑁, if-(𝐽 = 𝑁, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝐽)), if-(𝐽 = 𝑁, (𝑎‘𝐼)𝐸𝑧, (𝑎‘𝐼)𝐸(𝑎‘𝐽))))) |
| 115 | 85, 114 | pm2.61ian 812 |
. . . . . 6
⊢
(((((𝑁 ∈
ω ∧ 𝐼 ∈
ω ∧ 𝐽 ∈
ω) ∧ 𝑎 ∈
(𝑀 ↑m
ω)) ∧ 𝑧 ∈
𝑀) ∧ ({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁}))) ∈ (𝑀 ↑m ω)) →
((({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝐼)𝐸(({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝐽) ↔ if-(𝐼 = 𝑁, if-(𝐽 = 𝑁, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝐽)), if-(𝐽 = 𝑁, (𝑎‘𝐼)𝐸𝑧, (𝑎‘𝐼)𝐸(𝑎‘𝐽))))) |
| 116 | 48, 115 | bitrd 279 |
. . . . 5
⊢
(((((𝑁 ∈
ω ∧ 𝐼 ∈
ω ∧ 𝐽 ∈
ω) ∧ 𝑎 ∈
(𝑀 ↑m
ω)) ∧ 𝑧 ∈
𝑀) ∧ ({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁}))) ∈ (𝑀 ↑m ω)) →
((({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁}))) ∈ (𝑀 ↑m ω) ∧
(({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝐼)𝐸(({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝐽)) ↔ if-(𝐼 = 𝑁, if-(𝐽 = 𝑁, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝐽)), if-(𝐽 = 𝑁, (𝑎‘𝐼)𝐸𝑧, (𝑎‘𝐼)𝐸(𝑎‘𝐽))))) |
| 117 | 45, 116 | mpdan 687 |
. . . 4
⊢ ((((𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ 𝑎 ∈ (𝑀 ↑m ω)) ∧ 𝑧 ∈ 𝑀) → ((({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁}))) ∈ (𝑀 ↑m ω) ∧
(({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝐼)𝐸(({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁})))‘𝐽)) ↔ if-(𝐼 = 𝑁, if-(𝐽 = 𝑁, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝐽)), if-(𝐽 = 𝑁, (𝑎‘𝐼)𝐸𝑧, (𝑎‘𝐼)𝐸(𝑎‘𝐽))))) |
| 118 | 5, 117 | bitrd 279 |
. . 3
⊢ ((((𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ 𝑎 ∈ (𝑀 ↑m ω)) ∧ 𝑧 ∈ 𝑀) → (({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁}))) ∈ {𝑏 ∈ (𝑀 ↑m ω) ∣ (𝑏‘𝐼)𝐸(𝑏‘𝐽)} ↔ if-(𝐼 = 𝑁, if-(𝐽 = 𝑁, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝐽)), if-(𝐽 = 𝑁, (𝑎‘𝐼)𝐸𝑧, (𝑎‘𝐼)𝐸(𝑎‘𝐽))))) |
| 119 | 118 | ralbidva 3176 |
. 2
⊢ (((𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω) ∧ 𝑎 ∈ (𝑀 ↑m ω)) →
(∀𝑧 ∈ 𝑀 ({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁}))) ∈ {𝑏 ∈ (𝑀 ↑m ω) ∣ (𝑏‘𝐼)𝐸(𝑏‘𝐽)} ↔ ∀𝑧 ∈ 𝑀 if-(𝐼 = 𝑁, if-(𝐽 = 𝑁, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝐽)), if-(𝐽 = 𝑁, (𝑎‘𝐼)𝐸𝑧, (𝑎‘𝐼)𝐸(𝑎‘𝐽))))) |
| 120 | 119 | rabbidva 3443 |
1
⊢ ((𝑁 ∈ ω ∧ 𝐼 ∈ ω ∧ 𝐽 ∈ ω) → {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 ({〈𝑁, 𝑧〉} ∪ (𝑎 ↾ (ω ∖ {𝑁}))) ∈ {𝑏 ∈ (𝑀 ↑m ω) ∣ (𝑏‘𝐼)𝐸(𝑏‘𝐽)}} = {𝑎 ∈ (𝑀 ↑m ω) ∣
∀𝑧 ∈ 𝑀 if-(𝐼 = 𝑁, if-(𝐽 = 𝑁, 𝑧𝐸𝑧, 𝑧𝐸(𝑎‘𝐽)), if-(𝐽 = 𝑁, (𝑎‘𝐼)𝐸𝑧, (𝑎‘𝐼)𝐸(𝑎‘𝐽)))}) |