Step | Hyp | Ref
| Expression |
1 | | df-adds 33702 |
. . 3
⊢ +s =
norec2 ((𝑥 ∈ V, 𝑎 ∈ V ↦ (({𝑦 ∣ ∃𝑙 ∈ ( L
‘(1st ‘𝑥))𝑦 = (𝑙𝑎(2nd ‘𝑥))} ∪ {𝑧 ∣ ∃𝑙 ∈ ( L ‘(2nd
‘𝑥))𝑧 = ((1st ‘𝑥)𝑎𝑙)}) |s ({𝑦 ∣ ∃𝑟 ∈ ( R ‘(1st
‘𝑥))𝑦 = (𝑟𝑎(2nd ‘𝑥))} ∪ {𝑧 ∣ ∃𝑟 ∈ ( R ‘(2nd
‘𝑥))𝑧 = ((1st ‘𝑥)𝑎𝑟)})))) |
2 | 1 | norec2ov 33696 |
. 2
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (𝐴 +s 𝐵) = (〈𝐴, 𝐵〉(𝑥 ∈ V, 𝑎 ∈ V ↦ (({𝑦 ∣ ∃𝑙 ∈ ( L ‘(1st
‘𝑥))𝑦 = (𝑙𝑎(2nd ‘𝑥))} ∪ {𝑧 ∣ ∃𝑙 ∈ ( L ‘(2nd
‘𝑥))𝑧 = ((1st ‘𝑥)𝑎𝑙)}) |s ({𝑦 ∣ ∃𝑟 ∈ ( R ‘(1st
‘𝑥))𝑦 = (𝑟𝑎(2nd ‘𝑥))} ∪ {𝑧 ∣ ∃𝑟 ∈ ( R ‘(2nd
‘𝑥))𝑧 = ((1st ‘𝑥)𝑎𝑟)})))( +s ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉})))) |
3 | | opex 5328 |
. . . 4
⊢
〈𝐴, 𝐵〉 ∈ V |
4 | | addsfn 33708 |
. . . . . 6
⊢ +s Fn
( No × No
) |
5 | | fnfun 6439 |
. . . . . 6
⊢ ( +s Fn
( No × No )
→ Fun +s ) |
6 | 4, 5 | ax-mp 5 |
. . . . 5
⊢ Fun
+s |
7 | | fvex 6676 |
. . . . . . . . 9
⊢ ( L
‘𝐴) ∈
V |
8 | | fvex 6676 |
. . . . . . . . 9
⊢ ( R
‘𝐴) ∈
V |
9 | 7, 8 | unex 7473 |
. . . . . . . 8
⊢ (( L
‘𝐴) ∪ ( R
‘𝐴)) ∈
V |
10 | | snex 5304 |
. . . . . . . 8
⊢ {𝐴} ∈ V |
11 | 9, 10 | unex 7473 |
. . . . . . 7
⊢ ((( L
‘𝐴) ∪ ( R
‘𝐴)) ∪ {𝐴}) ∈ V |
12 | | fvex 6676 |
. . . . . . . . 9
⊢ ( L
‘𝐵) ∈
V |
13 | | fvex 6676 |
. . . . . . . . 9
⊢ ( R
‘𝐵) ∈
V |
14 | 12, 13 | unex 7473 |
. . . . . . . 8
⊢ (( L
‘𝐵) ∪ ( R
‘𝐵)) ∈
V |
15 | | snex 5304 |
. . . . . . . 8
⊢ {𝐵} ∈ V |
16 | 14, 15 | unex 7473 |
. . . . . . 7
⊢ ((( L
‘𝐵) ∪ ( R
‘𝐵)) ∪ {𝐵}) ∈ V |
17 | 11, 16 | xpex 7480 |
. . . . . 6
⊢ (((( L
‘𝐴) ∪ ( R
‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∈ V |
18 | 17 | difexi 5202 |
. . . . 5
⊢ ((((( L
‘𝐴) ∪ ( R
‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}) ∈ V |
19 | | resfunexg 6975 |
. . . . 5
⊢ ((Fun +s
∧ ((((( L ‘𝐴)
∪ ( R ‘𝐴)) ∪
{𝐴}) × ((( L
‘𝐵) ∪ ( R
‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}) ∈ V) → ( +s ↾ (((((
L ‘𝐴) ∪ ( R
‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉})) ∈ V) |
20 | 6, 18, 19 | mp2an 691 |
. . . 4
⊢ ( +s
↾ ((((( L ‘𝐴)
∪ ( R ‘𝐴)) ∪
{𝐴}) × ((( L
‘𝐵) ∪ ( R
‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉})) ∈ V |
21 | | 2fveq3 6668 |
. . . . . . . . 9
⊢ (𝑥 = 〈𝐴, 𝐵〉 → ( L ‘(1st
‘𝑥)) = ( L
‘(1st ‘〈𝐴, 𝐵〉))) |
22 | | fveq2 6663 |
. . . . . . . . . . 11
⊢ (𝑥 = 〈𝐴, 𝐵〉 → (2nd ‘𝑥) = (2nd
‘〈𝐴, 𝐵〉)) |
23 | 22 | oveq2d 7172 |
. . . . . . . . . 10
⊢ (𝑥 = 〈𝐴, 𝐵〉 → (𝑙𝑎(2nd ‘𝑥)) = (𝑙𝑎(2nd ‘〈𝐴, 𝐵〉))) |
24 | 23 | eqeq2d 2769 |
. . . . . . . . 9
⊢ (𝑥 = 〈𝐴, 𝐵〉 → (𝑦 = (𝑙𝑎(2nd ‘𝑥)) ↔ 𝑦 = (𝑙𝑎(2nd ‘〈𝐴, 𝐵〉)))) |
25 | 21, 24 | rexeqbidv 3320 |
. . . . . . . 8
⊢ (𝑥 = 〈𝐴, 𝐵〉 → (∃𝑙 ∈ ( L ‘(1st
‘𝑥))𝑦 = (𝑙𝑎(2nd ‘𝑥)) ↔ ∃𝑙 ∈ ( L ‘(1st
‘〈𝐴, 𝐵〉))𝑦 = (𝑙𝑎(2nd ‘〈𝐴, 𝐵〉)))) |
26 | 25 | abbidv 2822 |
. . . . . . 7
⊢ (𝑥 = 〈𝐴, 𝐵〉 → {𝑦 ∣ ∃𝑙 ∈ ( L ‘(1st
‘𝑥))𝑦 = (𝑙𝑎(2nd ‘𝑥))} = {𝑦 ∣ ∃𝑙 ∈ ( L ‘(1st
‘〈𝐴, 𝐵〉))𝑦 = (𝑙𝑎(2nd ‘〈𝐴, 𝐵〉))}) |
27 | | 2fveq3 6668 |
. . . . . . . . 9
⊢ (𝑥 = 〈𝐴, 𝐵〉 → ( L ‘(2nd
‘𝑥)) = ( L
‘(2nd ‘〈𝐴, 𝐵〉))) |
28 | | fveq2 6663 |
. . . . . . . . . . 11
⊢ (𝑥 = 〈𝐴, 𝐵〉 → (1st ‘𝑥) = (1st
‘〈𝐴, 𝐵〉)) |
29 | 28 | oveq1d 7171 |
. . . . . . . . . 10
⊢ (𝑥 = 〈𝐴, 𝐵〉 → ((1st ‘𝑥)𝑎𝑙) = ((1st ‘〈𝐴, 𝐵〉)𝑎𝑙)) |
30 | 29 | eqeq2d 2769 |
. . . . . . . . 9
⊢ (𝑥 = 〈𝐴, 𝐵〉 → (𝑧 = ((1st ‘𝑥)𝑎𝑙) ↔ 𝑧 = ((1st ‘〈𝐴, 𝐵〉)𝑎𝑙))) |
31 | 27, 30 | rexeqbidv 3320 |
. . . . . . . 8
⊢ (𝑥 = 〈𝐴, 𝐵〉 → (∃𝑙 ∈ ( L ‘(2nd
‘𝑥))𝑧 = ((1st ‘𝑥)𝑎𝑙) ↔ ∃𝑙 ∈ ( L ‘(2nd
‘〈𝐴, 𝐵〉))𝑧 = ((1st ‘〈𝐴, 𝐵〉)𝑎𝑙))) |
32 | 31 | abbidv 2822 |
. . . . . . 7
⊢ (𝑥 = 〈𝐴, 𝐵〉 → {𝑧 ∣ ∃𝑙 ∈ ( L ‘(2nd
‘𝑥))𝑧 = ((1st ‘𝑥)𝑎𝑙)} = {𝑧 ∣ ∃𝑙 ∈ ( L ‘(2nd
‘〈𝐴, 𝐵〉))𝑧 = ((1st ‘〈𝐴, 𝐵〉)𝑎𝑙)}) |
33 | 26, 32 | uneq12d 4071 |
. . . . . 6
⊢ (𝑥 = 〈𝐴, 𝐵〉 → ({𝑦 ∣ ∃𝑙 ∈ ( L ‘(1st
‘𝑥))𝑦 = (𝑙𝑎(2nd ‘𝑥))} ∪ {𝑧 ∣ ∃𝑙 ∈ ( L ‘(2nd
‘𝑥))𝑧 = ((1st ‘𝑥)𝑎𝑙)}) = ({𝑦 ∣ ∃𝑙 ∈ ( L ‘(1st
‘〈𝐴, 𝐵〉))𝑦 = (𝑙𝑎(2nd ‘〈𝐴, 𝐵〉))} ∪ {𝑧 ∣ ∃𝑙 ∈ ( L ‘(2nd
‘〈𝐴, 𝐵〉))𝑧 = ((1st ‘〈𝐴, 𝐵〉)𝑎𝑙)})) |
34 | | 2fveq3 6668 |
. . . . . . . . 9
⊢ (𝑥 = 〈𝐴, 𝐵〉 → ( R ‘(1st
‘𝑥)) = ( R
‘(1st ‘〈𝐴, 𝐵〉))) |
35 | 22 | oveq2d 7172 |
. . . . . . . . . 10
⊢ (𝑥 = 〈𝐴, 𝐵〉 → (𝑟𝑎(2nd ‘𝑥)) = (𝑟𝑎(2nd ‘〈𝐴, 𝐵〉))) |
36 | 35 | eqeq2d 2769 |
. . . . . . . . 9
⊢ (𝑥 = 〈𝐴, 𝐵〉 → (𝑦 = (𝑟𝑎(2nd ‘𝑥)) ↔ 𝑦 = (𝑟𝑎(2nd ‘〈𝐴, 𝐵〉)))) |
37 | 34, 36 | rexeqbidv 3320 |
. . . . . . . 8
⊢ (𝑥 = 〈𝐴, 𝐵〉 → (∃𝑟 ∈ ( R ‘(1st
‘𝑥))𝑦 = (𝑟𝑎(2nd ‘𝑥)) ↔ ∃𝑟 ∈ ( R ‘(1st
‘〈𝐴, 𝐵〉))𝑦 = (𝑟𝑎(2nd ‘〈𝐴, 𝐵〉)))) |
38 | 37 | abbidv 2822 |
. . . . . . 7
⊢ (𝑥 = 〈𝐴, 𝐵〉 → {𝑦 ∣ ∃𝑟 ∈ ( R ‘(1st
‘𝑥))𝑦 = (𝑟𝑎(2nd ‘𝑥))} = {𝑦 ∣ ∃𝑟 ∈ ( R ‘(1st
‘〈𝐴, 𝐵〉))𝑦 = (𝑟𝑎(2nd ‘〈𝐴, 𝐵〉))}) |
39 | | 2fveq3 6668 |
. . . . . . . . 9
⊢ (𝑥 = 〈𝐴, 𝐵〉 → ( R ‘(2nd
‘𝑥)) = ( R
‘(2nd ‘〈𝐴, 𝐵〉))) |
40 | 28 | oveq1d 7171 |
. . . . . . . . . 10
⊢ (𝑥 = 〈𝐴, 𝐵〉 → ((1st ‘𝑥)𝑎𝑟) = ((1st ‘〈𝐴, 𝐵〉)𝑎𝑟)) |
41 | 40 | eqeq2d 2769 |
. . . . . . . . 9
⊢ (𝑥 = 〈𝐴, 𝐵〉 → (𝑧 = ((1st ‘𝑥)𝑎𝑟) ↔ 𝑧 = ((1st ‘〈𝐴, 𝐵〉)𝑎𝑟))) |
42 | 39, 41 | rexeqbidv 3320 |
. . . . . . . 8
⊢ (𝑥 = 〈𝐴, 𝐵〉 → (∃𝑟 ∈ ( R ‘(2nd
‘𝑥))𝑧 = ((1st ‘𝑥)𝑎𝑟) ↔ ∃𝑟 ∈ ( R ‘(2nd
‘〈𝐴, 𝐵〉))𝑧 = ((1st ‘〈𝐴, 𝐵〉)𝑎𝑟))) |
43 | 42 | abbidv 2822 |
. . . . . . 7
⊢ (𝑥 = 〈𝐴, 𝐵〉 → {𝑧 ∣ ∃𝑟 ∈ ( R ‘(2nd
‘𝑥))𝑧 = ((1st ‘𝑥)𝑎𝑟)} = {𝑧 ∣ ∃𝑟 ∈ ( R ‘(2nd
‘〈𝐴, 𝐵〉))𝑧 = ((1st ‘〈𝐴, 𝐵〉)𝑎𝑟)}) |
44 | 38, 43 | uneq12d 4071 |
. . . . . 6
⊢ (𝑥 = 〈𝐴, 𝐵〉 → ({𝑦 ∣ ∃𝑟 ∈ ( R ‘(1st
‘𝑥))𝑦 = (𝑟𝑎(2nd ‘𝑥))} ∪ {𝑧 ∣ ∃𝑟 ∈ ( R ‘(2nd
‘𝑥))𝑧 = ((1st ‘𝑥)𝑎𝑟)}) = ({𝑦 ∣ ∃𝑟 ∈ ( R ‘(1st
‘〈𝐴, 𝐵〉))𝑦 = (𝑟𝑎(2nd ‘〈𝐴, 𝐵〉))} ∪ {𝑧 ∣ ∃𝑟 ∈ ( R ‘(2nd
‘〈𝐴, 𝐵〉))𝑧 = ((1st ‘〈𝐴, 𝐵〉)𝑎𝑟)})) |
45 | 33, 44 | oveq12d 7174 |
. . . . 5
⊢ (𝑥 = 〈𝐴, 𝐵〉 → (({𝑦 ∣ ∃𝑙 ∈ ( L ‘(1st
‘𝑥))𝑦 = (𝑙𝑎(2nd ‘𝑥))} ∪ {𝑧 ∣ ∃𝑙 ∈ ( L ‘(2nd
‘𝑥))𝑧 = ((1st ‘𝑥)𝑎𝑙)}) |s ({𝑦 ∣ ∃𝑟 ∈ ( R ‘(1st
‘𝑥))𝑦 = (𝑟𝑎(2nd ‘𝑥))} ∪ {𝑧 ∣ ∃𝑟 ∈ ( R ‘(2nd
‘𝑥))𝑧 = ((1st ‘𝑥)𝑎𝑟)})) = (({𝑦 ∣ ∃𝑙 ∈ ( L ‘(1st
‘〈𝐴, 𝐵〉))𝑦 = (𝑙𝑎(2nd ‘〈𝐴, 𝐵〉))} ∪ {𝑧 ∣ ∃𝑙 ∈ ( L ‘(2nd
‘〈𝐴, 𝐵〉))𝑧 = ((1st ‘〈𝐴, 𝐵〉)𝑎𝑙)}) |s ({𝑦 ∣ ∃𝑟 ∈ ( R ‘(1st
‘〈𝐴, 𝐵〉))𝑦 = (𝑟𝑎(2nd ‘〈𝐴, 𝐵〉))} ∪ {𝑧 ∣ ∃𝑟 ∈ ( R ‘(2nd
‘〈𝐴, 𝐵〉))𝑧 = ((1st ‘〈𝐴, 𝐵〉)𝑎𝑟)}))) |
46 | | oveq 7162 |
. . . . . . . . . 10
⊢ (𝑎 = ( +s ↾ ((((( L
‘𝐴) ∪ ( R
‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉})) → (𝑙𝑎(2nd ‘〈𝐴, 𝐵〉)) = (𝑙( +s ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))(2nd ‘〈𝐴, 𝐵〉))) |
47 | 46 | eqeq2d 2769 |
. . . . . . . . 9
⊢ (𝑎 = ( +s ↾ ((((( L
‘𝐴) ∪ ( R
‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉})) → (𝑦 = (𝑙𝑎(2nd ‘〈𝐴, 𝐵〉)) ↔ 𝑦 = (𝑙( +s ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))(2nd ‘〈𝐴, 𝐵〉)))) |
48 | 47 | rexbidv 3221 |
. . . . . . . 8
⊢ (𝑎 = ( +s ↾ ((((( L
‘𝐴) ∪ ( R
‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉})) → (∃𝑙 ∈ ( L ‘(1st
‘〈𝐴, 𝐵〉))𝑦 = (𝑙𝑎(2nd ‘〈𝐴, 𝐵〉)) ↔ ∃𝑙 ∈ ( L ‘(1st
‘〈𝐴, 𝐵〉))𝑦 = (𝑙( +s ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))(2nd ‘〈𝐴, 𝐵〉)))) |
49 | 48 | abbidv 2822 |
. . . . . . 7
⊢ (𝑎 = ( +s ↾ ((((( L
‘𝐴) ∪ ( R
‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉})) → {𝑦 ∣ ∃𝑙 ∈ ( L ‘(1st
‘〈𝐴, 𝐵〉))𝑦 = (𝑙𝑎(2nd ‘〈𝐴, 𝐵〉))} = {𝑦 ∣ ∃𝑙 ∈ ( L ‘(1st
‘〈𝐴, 𝐵〉))𝑦 = (𝑙( +s ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))(2nd ‘〈𝐴, 𝐵〉))}) |
50 | | oveq 7162 |
. . . . . . . . . 10
⊢ (𝑎 = ( +s ↾ ((((( L
‘𝐴) ∪ ( R
‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉})) → ((1st
‘〈𝐴, 𝐵〉)𝑎𝑙) = ((1st ‘〈𝐴, 𝐵〉)( +s ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))𝑙)) |
51 | 50 | eqeq2d 2769 |
. . . . . . . . 9
⊢ (𝑎 = ( +s ↾ ((((( L
‘𝐴) ∪ ( R
‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉})) → (𝑧 = ((1st ‘〈𝐴, 𝐵〉)𝑎𝑙) ↔ 𝑧 = ((1st ‘〈𝐴, 𝐵〉)( +s ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))𝑙))) |
52 | 51 | rexbidv 3221 |
. . . . . . . 8
⊢ (𝑎 = ( +s ↾ ((((( L
‘𝐴) ∪ ( R
‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉})) → (∃𝑙 ∈ ( L ‘(2nd
‘〈𝐴, 𝐵〉))𝑧 = ((1st ‘〈𝐴, 𝐵〉)𝑎𝑙) ↔ ∃𝑙 ∈ ( L ‘(2nd
‘〈𝐴, 𝐵〉))𝑧 = ((1st ‘〈𝐴, 𝐵〉)( +s ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))𝑙))) |
53 | 52 | abbidv 2822 |
. . . . . . 7
⊢ (𝑎 = ( +s ↾ ((((( L
‘𝐴) ∪ ( R
‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉})) → {𝑧 ∣ ∃𝑙 ∈ ( L ‘(2nd
‘〈𝐴, 𝐵〉))𝑧 = ((1st ‘〈𝐴, 𝐵〉)𝑎𝑙)} = {𝑧 ∣ ∃𝑙 ∈ ( L ‘(2nd
‘〈𝐴, 𝐵〉))𝑧 = ((1st ‘〈𝐴, 𝐵〉)( +s ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))𝑙)}) |
54 | 49, 53 | uneq12d 4071 |
. . . . . 6
⊢ (𝑎 = ( +s ↾ ((((( L
‘𝐴) ∪ ( R
‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉})) → ({𝑦 ∣ ∃𝑙 ∈ ( L ‘(1st
‘〈𝐴, 𝐵〉))𝑦 = (𝑙𝑎(2nd ‘〈𝐴, 𝐵〉))} ∪ {𝑧 ∣ ∃𝑙 ∈ ( L ‘(2nd
‘〈𝐴, 𝐵〉))𝑧 = ((1st ‘〈𝐴, 𝐵〉)𝑎𝑙)}) = ({𝑦 ∣ ∃𝑙 ∈ ( L ‘(1st
‘〈𝐴, 𝐵〉))𝑦 = (𝑙( +s ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))(2nd ‘〈𝐴, 𝐵〉))} ∪ {𝑧 ∣ ∃𝑙 ∈ ( L ‘(2nd
‘〈𝐴, 𝐵〉))𝑧 = ((1st ‘〈𝐴, 𝐵〉)( +s ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))𝑙)})) |
55 | | oveq 7162 |
. . . . . . . . . 10
⊢ (𝑎 = ( +s ↾ ((((( L
‘𝐴) ∪ ( R
‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉})) → (𝑟𝑎(2nd ‘〈𝐴, 𝐵〉)) = (𝑟( +s ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))(2nd ‘〈𝐴, 𝐵〉))) |
56 | 55 | eqeq2d 2769 |
. . . . . . . . 9
⊢ (𝑎 = ( +s ↾ ((((( L
‘𝐴) ∪ ( R
‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉})) → (𝑦 = (𝑟𝑎(2nd ‘〈𝐴, 𝐵〉)) ↔ 𝑦 = (𝑟( +s ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))(2nd ‘〈𝐴, 𝐵〉)))) |
57 | 56 | rexbidv 3221 |
. . . . . . . 8
⊢ (𝑎 = ( +s ↾ ((((( L
‘𝐴) ∪ ( R
‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉})) → (∃𝑟 ∈ ( R ‘(1st
‘〈𝐴, 𝐵〉))𝑦 = (𝑟𝑎(2nd ‘〈𝐴, 𝐵〉)) ↔ ∃𝑟 ∈ ( R ‘(1st
‘〈𝐴, 𝐵〉))𝑦 = (𝑟( +s ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))(2nd ‘〈𝐴, 𝐵〉)))) |
58 | 57 | abbidv 2822 |
. . . . . . 7
⊢ (𝑎 = ( +s ↾ ((((( L
‘𝐴) ∪ ( R
‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉})) → {𝑦 ∣ ∃𝑟 ∈ ( R ‘(1st
‘〈𝐴, 𝐵〉))𝑦 = (𝑟𝑎(2nd ‘〈𝐴, 𝐵〉))} = {𝑦 ∣ ∃𝑟 ∈ ( R ‘(1st
‘〈𝐴, 𝐵〉))𝑦 = (𝑟( +s ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))(2nd ‘〈𝐴, 𝐵〉))}) |
59 | | oveq 7162 |
. . . . . . . . . 10
⊢ (𝑎 = ( +s ↾ ((((( L
‘𝐴) ∪ ( R
‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉})) → ((1st
‘〈𝐴, 𝐵〉)𝑎𝑟) = ((1st ‘〈𝐴, 𝐵〉)( +s ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))𝑟)) |
60 | 59 | eqeq2d 2769 |
. . . . . . . . 9
⊢ (𝑎 = ( +s ↾ ((((( L
‘𝐴) ∪ ( R
‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉})) → (𝑧 = ((1st ‘〈𝐴, 𝐵〉)𝑎𝑟) ↔ 𝑧 = ((1st ‘〈𝐴, 𝐵〉)( +s ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))𝑟))) |
61 | 60 | rexbidv 3221 |
. . . . . . . 8
⊢ (𝑎 = ( +s ↾ ((((( L
‘𝐴) ∪ ( R
‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉})) → (∃𝑟 ∈ ( R ‘(2nd
‘〈𝐴, 𝐵〉))𝑧 = ((1st ‘〈𝐴, 𝐵〉)𝑎𝑟) ↔ ∃𝑟 ∈ ( R ‘(2nd
‘〈𝐴, 𝐵〉))𝑧 = ((1st ‘〈𝐴, 𝐵〉)( +s ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))𝑟))) |
62 | 61 | abbidv 2822 |
. . . . . . 7
⊢ (𝑎 = ( +s ↾ ((((( L
‘𝐴) ∪ ( R
‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉})) → {𝑧 ∣ ∃𝑟 ∈ ( R ‘(2nd
‘〈𝐴, 𝐵〉))𝑧 = ((1st ‘〈𝐴, 𝐵〉)𝑎𝑟)} = {𝑧 ∣ ∃𝑟 ∈ ( R ‘(2nd
‘〈𝐴, 𝐵〉))𝑧 = ((1st ‘〈𝐴, 𝐵〉)( +s ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))𝑟)}) |
63 | 58, 62 | uneq12d 4071 |
. . . . . 6
⊢ (𝑎 = ( +s ↾ ((((( L
‘𝐴) ∪ ( R
‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉})) → ({𝑦 ∣ ∃𝑟 ∈ ( R ‘(1st
‘〈𝐴, 𝐵〉))𝑦 = (𝑟𝑎(2nd ‘〈𝐴, 𝐵〉))} ∪ {𝑧 ∣ ∃𝑟 ∈ ( R ‘(2nd
‘〈𝐴, 𝐵〉))𝑧 = ((1st ‘〈𝐴, 𝐵〉)𝑎𝑟)}) = ({𝑦 ∣ ∃𝑟 ∈ ( R ‘(1st
‘〈𝐴, 𝐵〉))𝑦 = (𝑟( +s ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))(2nd ‘〈𝐴, 𝐵〉))} ∪ {𝑧 ∣ ∃𝑟 ∈ ( R ‘(2nd
‘〈𝐴, 𝐵〉))𝑧 = ((1st ‘〈𝐴, 𝐵〉)( +s ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))𝑟)})) |
64 | 54, 63 | oveq12d 7174 |
. . . . 5
⊢ (𝑎 = ( +s ↾ ((((( L
‘𝐴) ∪ ( R
‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉})) → (({𝑦 ∣ ∃𝑙 ∈ ( L ‘(1st
‘〈𝐴, 𝐵〉))𝑦 = (𝑙𝑎(2nd ‘〈𝐴, 𝐵〉))} ∪ {𝑧 ∣ ∃𝑙 ∈ ( L ‘(2nd
‘〈𝐴, 𝐵〉))𝑧 = ((1st ‘〈𝐴, 𝐵〉)𝑎𝑙)}) |s ({𝑦 ∣ ∃𝑟 ∈ ( R ‘(1st
‘〈𝐴, 𝐵〉))𝑦 = (𝑟𝑎(2nd ‘〈𝐴, 𝐵〉))} ∪ {𝑧 ∣ ∃𝑟 ∈ ( R ‘(2nd
‘〈𝐴, 𝐵〉))𝑧 = ((1st ‘〈𝐴, 𝐵〉)𝑎𝑟)})) = (({𝑦 ∣ ∃𝑙 ∈ ( L ‘(1st
‘〈𝐴, 𝐵〉))𝑦 = (𝑙( +s ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))(2nd ‘〈𝐴, 𝐵〉))} ∪ {𝑧 ∣ ∃𝑙 ∈ ( L ‘(2nd
‘〈𝐴, 𝐵〉))𝑧 = ((1st ‘〈𝐴, 𝐵〉)( +s ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))𝑙)}) |s ({𝑦 ∣ ∃𝑟 ∈ ( R ‘(1st
‘〈𝐴, 𝐵〉))𝑦 = (𝑟( +s ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))(2nd ‘〈𝐴, 𝐵〉))} ∪ {𝑧 ∣ ∃𝑟 ∈ ( R ‘(2nd
‘〈𝐴, 𝐵〉))𝑧 = ((1st ‘〈𝐴, 𝐵〉)( +s ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))𝑟)}))) |
65 | | eqid 2758 |
. . . . 5
⊢ (𝑥 ∈ V, 𝑎 ∈ V ↦ (({𝑦 ∣ ∃𝑙 ∈ ( L ‘(1st
‘𝑥))𝑦 = (𝑙𝑎(2nd ‘𝑥))} ∪ {𝑧 ∣ ∃𝑙 ∈ ( L ‘(2nd
‘𝑥))𝑧 = ((1st ‘𝑥)𝑎𝑙)}) |s ({𝑦 ∣ ∃𝑟 ∈ ( R ‘(1st
‘𝑥))𝑦 = (𝑟𝑎(2nd ‘𝑥))} ∪ {𝑧 ∣ ∃𝑟 ∈ ( R ‘(2nd
‘𝑥))𝑧 = ((1st ‘𝑥)𝑎𝑟)}))) = (𝑥 ∈ V, 𝑎 ∈ V ↦ (({𝑦 ∣ ∃𝑙 ∈ ( L ‘(1st
‘𝑥))𝑦 = (𝑙𝑎(2nd ‘𝑥))} ∪ {𝑧 ∣ ∃𝑙 ∈ ( L ‘(2nd
‘𝑥))𝑧 = ((1st ‘𝑥)𝑎𝑙)}) |s ({𝑦 ∣ ∃𝑟 ∈ ( R ‘(1st
‘𝑥))𝑦 = (𝑟𝑎(2nd ‘𝑥))} ∪ {𝑧 ∣ ∃𝑟 ∈ ( R ‘(2nd
‘𝑥))𝑧 = ((1st ‘𝑥)𝑎𝑟)}))) |
66 | | ovex 7189 |
. . . . 5
⊢ (({𝑦 ∣ ∃𝑙 ∈ ( L
‘(1st ‘〈𝐴, 𝐵〉))𝑦 = (𝑙( +s ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))(2nd ‘〈𝐴, 𝐵〉))} ∪ {𝑧 ∣ ∃𝑙 ∈ ( L ‘(2nd
‘〈𝐴, 𝐵〉))𝑧 = ((1st ‘〈𝐴, 𝐵〉)( +s ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))𝑙)}) |s ({𝑦 ∣ ∃𝑟 ∈ ( R ‘(1st
‘〈𝐴, 𝐵〉))𝑦 = (𝑟( +s ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))(2nd ‘〈𝐴, 𝐵〉))} ∪ {𝑧 ∣ ∃𝑟 ∈ ( R ‘(2nd
‘〈𝐴, 𝐵〉))𝑧 = ((1st ‘〈𝐴, 𝐵〉)( +s ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))𝑟)})) ∈ V |
67 | 45, 64, 65, 66 | ovmpo 7311 |
. . . 4
⊢
((〈𝐴, 𝐵〉 ∈ V ∧ ( +s
↾ ((((( L ‘𝐴)
∪ ( R ‘𝐴)) ∪
{𝐴}) × ((( L
‘𝐵) ∪ ( R
‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉})) ∈ V) → (〈𝐴, 𝐵〉(𝑥 ∈ V, 𝑎 ∈ V ↦ (({𝑦 ∣ ∃𝑙 ∈ ( L ‘(1st
‘𝑥))𝑦 = (𝑙𝑎(2nd ‘𝑥))} ∪ {𝑧 ∣ ∃𝑙 ∈ ( L ‘(2nd
‘𝑥))𝑧 = ((1st ‘𝑥)𝑎𝑙)}) |s ({𝑦 ∣ ∃𝑟 ∈ ( R ‘(1st
‘𝑥))𝑦 = (𝑟𝑎(2nd ‘𝑥))} ∪ {𝑧 ∣ ∃𝑟 ∈ ( R ‘(2nd
‘𝑥))𝑧 = ((1st ‘𝑥)𝑎𝑟)})))( +s ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))) = (({𝑦 ∣ ∃𝑙 ∈ ( L ‘(1st
‘〈𝐴, 𝐵〉))𝑦 = (𝑙( +s ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))(2nd ‘〈𝐴, 𝐵〉))} ∪ {𝑧 ∣ ∃𝑙 ∈ ( L ‘(2nd
‘〈𝐴, 𝐵〉))𝑧 = ((1st ‘〈𝐴, 𝐵〉)( +s ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))𝑙)}) |s ({𝑦 ∣ ∃𝑟 ∈ ( R ‘(1st
‘〈𝐴, 𝐵〉))𝑦 = (𝑟( +s ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))(2nd ‘〈𝐴, 𝐵〉))} ∪ {𝑧 ∣ ∃𝑟 ∈ ( R ‘(2nd
‘〈𝐴, 𝐵〉))𝑧 = ((1st ‘〈𝐴, 𝐵〉)( +s ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))𝑟)}))) |
68 | 3, 20, 67 | mp2an 691 |
. . 3
⊢
(〈𝐴, 𝐵〉(𝑥 ∈ V, 𝑎 ∈ V ↦ (({𝑦 ∣ ∃𝑙 ∈ ( L ‘(1st
‘𝑥))𝑦 = (𝑙𝑎(2nd ‘𝑥))} ∪ {𝑧 ∣ ∃𝑙 ∈ ( L ‘(2nd
‘𝑥))𝑧 = ((1st ‘𝑥)𝑎𝑙)}) |s ({𝑦 ∣ ∃𝑟 ∈ ( R ‘(1st
‘𝑥))𝑦 = (𝑟𝑎(2nd ‘𝑥))} ∪ {𝑧 ∣ ∃𝑟 ∈ ( R ‘(2nd
‘𝑥))𝑧 = ((1st ‘𝑥)𝑎𝑟)})))( +s ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))) = (({𝑦 ∣ ∃𝑙 ∈ ( L ‘(1st
‘〈𝐴, 𝐵〉))𝑦 = (𝑙( +s ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))(2nd ‘〈𝐴, 𝐵〉))} ∪ {𝑧 ∣ ∃𝑙 ∈ ( L ‘(2nd
‘〈𝐴, 𝐵〉))𝑧 = ((1st ‘〈𝐴, 𝐵〉)( +s ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))𝑙)}) |s ({𝑦 ∣ ∃𝑟 ∈ ( R ‘(1st
‘〈𝐴, 𝐵〉))𝑦 = (𝑟( +s ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))(2nd ‘〈𝐴, 𝐵〉))} ∪ {𝑧 ∣ ∃𝑟 ∈ ( R ‘(2nd
‘〈𝐴, 𝐵〉))𝑧 = ((1st ‘〈𝐴, 𝐵〉)( +s ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))𝑟)})) |
69 | | op1stg 7711 |
. . . . . . . 8
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (1st ‘〈𝐴, 𝐵〉) = 𝐴) |
70 | 69 | fveq2d 6667 |
. . . . . . 7
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → ( L ‘(1st
‘〈𝐴, 𝐵〉)) = ( L ‘𝐴)) |
71 | 70 | eleq2d 2837 |
. . . . . . . . 9
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (𝑙 ∈ ( L ‘(1st
‘〈𝐴, 𝐵〉)) ↔ 𝑙 ∈ ( L ‘𝐴))) |
72 | | op2ndg 7712 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (2nd ‘〈𝐴, 𝐵〉) = 𝐵) |
73 | 72 | adantr 484 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑙 ∈ ( L ‘𝐴)) → (2nd ‘〈𝐴, 𝐵〉) = 𝐵) |
74 | 73 | oveq2d 7172 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑙 ∈ ( L ‘𝐴)) → (𝑙( +s ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))(2nd ‘〈𝐴, 𝐵〉)) = (𝑙( +s ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))𝐵)) |
75 | | elun1 4083 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑙 ∈ ( L ‘𝐴) → 𝑙 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))) |
76 | | elun1 4083 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑙 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴)) → 𝑙 ∈ ((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴})) |
77 | 75, 76 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑙 ∈ ( L ‘𝐴) → 𝑙 ∈ ((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴})) |
78 | 77 | adantl 485 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑙 ∈ ( L ‘𝐴)) → 𝑙 ∈ ((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴})) |
79 | | snidg 4559 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐵 ∈
No → 𝐵 ∈
{𝐵}) |
80 | | elun2 4084 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐵 ∈ {𝐵} → 𝐵 ∈ ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) |
81 | 79, 80 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐵 ∈
No → 𝐵 ∈
((( L ‘𝐵) ∪ ( R
‘𝐵)) ∪ {𝐵})) |
82 | 81 | adantl 485 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → 𝐵 ∈ ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) |
83 | 82 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑙 ∈ ( L ‘𝐴)) → 𝐵 ∈ ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) |
84 | 78, 83 | opelxpd 5566 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑙 ∈ ( L ‘𝐴)) → 〈𝑙, 𝐵〉 ∈ (((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵}))) |
85 | | leftirr 33664 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐴 ∈
No → ¬ 𝐴
∈ ( L ‘𝐴)) |
86 | 85 | adantr 484 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → ¬ 𝐴 ∈ ( L ‘𝐴)) |
87 | | eleq1 2839 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑙 = 𝐴 → (𝑙 ∈ ( L ‘𝐴) ↔ 𝐴 ∈ ( L ‘𝐴))) |
88 | 87 | notbid 321 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑙 = 𝐴 → (¬ 𝑙 ∈ ( L ‘𝐴) ↔ ¬ 𝐴 ∈ ( L ‘𝐴))) |
89 | 86, 88 | syl5ibrcom 250 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (𝑙 = 𝐴 → ¬ 𝑙 ∈ ( L ‘𝐴))) |
90 | 89 | necon2ad 2966 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (𝑙 ∈ ( L ‘𝐴) → 𝑙 ≠ 𝐴)) |
91 | 90 | imp 410 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑙 ∈ ( L ‘𝐴)) → 𝑙 ≠ 𝐴) |
92 | 91 | orcd 870 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑙 ∈ ( L ‘𝐴)) → (𝑙 ≠ 𝐴 ∨ 𝐵 ≠ 𝐵)) |
93 | | simpr 488 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑙 ∈ ( L ‘𝐴)) → 𝑙 ∈ ( L ‘𝐴)) |
94 | | simplr 768 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑙 ∈ ( L ‘𝐴)) → 𝐵 ∈ No
) |
95 | | opthneg 5345 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑙 ∈ ( L ‘𝐴) ∧ 𝐵 ∈ No )
→ (〈𝑙, 𝐵〉 ≠ 〈𝐴, 𝐵〉 ↔ (𝑙 ≠ 𝐴 ∨ 𝐵 ≠ 𝐵))) |
96 | 93, 94, 95 | syl2anc 587 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑙 ∈ ( L ‘𝐴)) → (〈𝑙, 𝐵〉 ≠ 〈𝐴, 𝐵〉 ↔ (𝑙 ≠ 𝐴 ∨ 𝐵 ≠ 𝐵))) |
97 | 92, 96 | mpbird 260 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑙 ∈ ( L ‘𝐴)) → 〈𝑙, 𝐵〉 ≠ 〈𝐴, 𝐵〉) |
98 | | eldifsn 4680 |
. . . . . . . . . . . . . . 15
⊢
(〈𝑙, 𝐵〉 ∈ ((((( L
‘𝐴) ∪ ( R
‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}) ↔ (〈𝑙, 𝐵〉 ∈ (((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∧ 〈𝑙, 𝐵〉 ≠ 〈𝐴, 𝐵〉)) |
99 | 84, 97, 98 | sylanbrc 586 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑙 ∈ ( L ‘𝐴)) → 〈𝑙, 𝐵〉 ∈ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉})) |
100 | 99 | fvresd 6683 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑙 ∈ ( L ‘𝐴)) → (( +s ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))‘〈𝑙, 𝐵〉) = ( +s ‘〈𝑙, 𝐵〉)) |
101 | | df-ov 7159 |
. . . . . . . . . . . . 13
⊢ (𝑙( +s ↾ ((((( L
‘𝐴) ∪ ( R
‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))𝐵) = (( +s ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))‘〈𝑙, 𝐵〉) |
102 | | df-ov 7159 |
. . . . . . . . . . . . 13
⊢ (𝑙 +s 𝐵) = ( +s ‘〈𝑙, 𝐵〉) |
103 | 100, 101,
102 | 3eqtr4g 2818 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑙 ∈ ( L ‘𝐴)) → (𝑙( +s ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))𝐵) = (𝑙 +s 𝐵)) |
104 | 74, 103 | eqtrd 2793 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑙 ∈ ( L ‘𝐴)) → (𝑙( +s ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))(2nd ‘〈𝐴, 𝐵〉)) = (𝑙 +s 𝐵)) |
105 | 104 | eqeq2d 2769 |
. . . . . . . . . 10
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑙 ∈ ( L ‘𝐴)) → (𝑦 = (𝑙( +s ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))(2nd ‘〈𝐴, 𝐵〉)) ↔ 𝑦 = (𝑙 +s 𝐵))) |
106 | 105 | ex 416 |
. . . . . . . . 9
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (𝑙 ∈ ( L ‘𝐴) → (𝑦 = (𝑙( +s ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))(2nd ‘〈𝐴, 𝐵〉)) ↔ 𝑦 = (𝑙 +s 𝐵)))) |
107 | 71, 106 | sylbid 243 |
. . . . . . . 8
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (𝑙 ∈ ( L ‘(1st
‘〈𝐴, 𝐵〉)) → (𝑦 = (𝑙( +s ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))(2nd ‘〈𝐴, 𝐵〉)) ↔ 𝑦 = (𝑙 +s 𝐵)))) |
108 | 107 | imp 410 |
. . . . . . 7
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑙 ∈ ( L ‘(1st
‘〈𝐴, 𝐵〉))) → (𝑦 = (𝑙( +s ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))(2nd ‘〈𝐴, 𝐵〉)) ↔ 𝑦 = (𝑙 +s 𝐵))) |
109 | 70, 108 | rexeqbidva 3336 |
. . . . . 6
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (∃𝑙 ∈ ( L ‘(1st
‘〈𝐴, 𝐵〉))𝑦 = (𝑙( +s ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))(2nd ‘〈𝐴, 𝐵〉)) ↔ ∃𝑙 ∈ ( L ‘𝐴)𝑦 = (𝑙 +s 𝐵))) |
110 | 109 | abbidv 2822 |
. . . . 5
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → {𝑦 ∣ ∃𝑙 ∈ ( L ‘(1st
‘〈𝐴, 𝐵〉))𝑦 = (𝑙( +s ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))(2nd ‘〈𝐴, 𝐵〉))} = {𝑦 ∣ ∃𝑙 ∈ ( L ‘𝐴)𝑦 = (𝑙 +s 𝐵)}) |
111 | 72 | fveq2d 6667 |
. . . . . . 7
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → ( L ‘(2nd
‘〈𝐴, 𝐵〉)) = ( L ‘𝐵)) |
112 | 111 | eleq2d 2837 |
. . . . . . . . 9
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (𝑙 ∈ ( L ‘(2nd
‘〈𝐴, 𝐵〉)) ↔ 𝑙 ∈ ( L ‘𝐵))) |
113 | 69 | adantr 484 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑙 ∈ ( L ‘𝐵)) → (1st ‘〈𝐴, 𝐵〉) = 𝐴) |
114 | 113 | oveq1d 7171 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑙 ∈ ( L ‘𝐵)) → ((1st
‘〈𝐴, 𝐵〉)( +s ↾ ((((( L
‘𝐴) ∪ ( R
‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))𝑙) = (𝐴( +s ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))𝑙)) |
115 | | snidg 4559 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐴 ∈
No → 𝐴 ∈
{𝐴}) |
116 | 115 | adantr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → 𝐴 ∈ {𝐴}) |
117 | | elun2 4084 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 ∈ {𝐴} → 𝐴 ∈ ((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴})) |
118 | 116, 117 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → 𝐴 ∈ ((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴})) |
119 | 118 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑙 ∈ ( L ‘𝐵)) → 𝐴 ∈ ((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴})) |
120 | | elun1 4083 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑙 ∈ ( L ‘𝐵) → 𝑙 ∈ (( L ‘𝐵) ∪ ( R ‘𝐵))) |
121 | | elun1 4083 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑙 ∈ (( L ‘𝐵) ∪ ( R ‘𝐵)) → 𝑙 ∈ ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) |
122 | 120, 121 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑙 ∈ ( L ‘𝐵) → 𝑙 ∈ ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) |
123 | 122 | adantl 485 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑙 ∈ ( L ‘𝐵)) → 𝑙 ∈ ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) |
124 | 119, 123 | opelxpd 5566 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑙 ∈ ( L ‘𝐵)) → 〈𝐴, 𝑙〉 ∈ (((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵}))) |
125 | | leftirr 33664 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐵 ∈
No → ¬ 𝐵
∈ ( L ‘𝐵)) |
126 | 125 | adantl 485 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → ¬ 𝐵 ∈ ( L ‘𝐵)) |
127 | | eleq1 2839 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑙 = 𝐵 → (𝑙 ∈ ( L ‘𝐵) ↔ 𝐵 ∈ ( L ‘𝐵))) |
128 | 127 | notbid 321 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑙 = 𝐵 → (¬ 𝑙 ∈ ( L ‘𝐵) ↔ ¬ 𝐵 ∈ ( L ‘𝐵))) |
129 | 126, 128 | syl5ibrcom 250 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (𝑙 = 𝐵 → ¬ 𝑙 ∈ ( L ‘𝐵))) |
130 | 129 | necon2ad 2966 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (𝑙 ∈ ( L ‘𝐵) → 𝑙 ≠ 𝐵)) |
131 | 130 | imp 410 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑙 ∈ ( L ‘𝐵)) → 𝑙 ≠ 𝐵) |
132 | 131 | olcd 871 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑙 ∈ ( L ‘𝐵)) → (𝐴 ≠ 𝐴 ∨ 𝑙 ≠ 𝐵)) |
133 | | opthneg 5345 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈
No ∧ 𝑙 ∈ (
L ‘𝐵)) →
(〈𝐴, 𝑙〉 ≠ 〈𝐴, 𝐵〉 ↔ (𝐴 ≠ 𝐴 ∨ 𝑙 ≠ 𝐵))) |
134 | 133 | adantlr 714 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑙 ∈ ( L ‘𝐵)) → (〈𝐴, 𝑙〉 ≠ 〈𝐴, 𝐵〉 ↔ (𝐴 ≠ 𝐴 ∨ 𝑙 ≠ 𝐵))) |
135 | 132, 134 | mpbird 260 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑙 ∈ ( L ‘𝐵)) → 〈𝐴, 𝑙〉 ≠ 〈𝐴, 𝐵〉) |
136 | | eldifsn 4680 |
. . . . . . . . . . . . . . 15
⊢
(〈𝐴, 𝑙〉 ∈ ((((( L
‘𝐴) ∪ ( R
‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}) ↔ (〈𝐴, 𝑙〉 ∈ (((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∧ 〈𝐴, 𝑙〉 ≠ 〈𝐴, 𝐵〉)) |
137 | 124, 135,
136 | sylanbrc 586 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑙 ∈ ( L ‘𝐵)) → 〈𝐴, 𝑙〉 ∈ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉})) |
138 | 137 | fvresd 6683 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑙 ∈ ( L ‘𝐵)) → (( +s ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))‘〈𝐴, 𝑙〉) = ( +s ‘〈𝐴, 𝑙〉)) |
139 | | df-ov 7159 |
. . . . . . . . . . . . 13
⊢ (𝐴( +s ↾ ((((( L
‘𝐴) ∪ ( R
‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))𝑙) = (( +s ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))‘〈𝐴, 𝑙〉) |
140 | | df-ov 7159 |
. . . . . . . . . . . . 13
⊢ (𝐴 +s 𝑙) = ( +s ‘〈𝐴, 𝑙〉) |
141 | 138, 139,
140 | 3eqtr4g 2818 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑙 ∈ ( L ‘𝐵)) → (𝐴( +s ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))𝑙) = (𝐴 +s 𝑙)) |
142 | 114, 141 | eqtrd 2793 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑙 ∈ ( L ‘𝐵)) → ((1st
‘〈𝐴, 𝐵〉)( +s ↾ ((((( L
‘𝐴) ∪ ( R
‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))𝑙) = (𝐴 +s 𝑙)) |
143 | 142 | eqeq2d 2769 |
. . . . . . . . . 10
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑙 ∈ ( L ‘𝐵)) → (𝑧 = ((1st ‘〈𝐴, 𝐵〉)( +s ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))𝑙) ↔ 𝑧 = (𝐴 +s 𝑙))) |
144 | 143 | ex 416 |
. . . . . . . . 9
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (𝑙 ∈ ( L ‘𝐵) → (𝑧 = ((1st ‘〈𝐴, 𝐵〉)( +s ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))𝑙) ↔ 𝑧 = (𝐴 +s 𝑙)))) |
145 | 112, 144 | sylbid 243 |
. . . . . . . 8
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (𝑙 ∈ ( L ‘(2nd
‘〈𝐴, 𝐵〉)) → (𝑧 = ((1st
‘〈𝐴, 𝐵〉)( +s ↾ ((((( L
‘𝐴) ∪ ( R
‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))𝑙) ↔ 𝑧 = (𝐴 +s 𝑙)))) |
146 | 145 | imp 410 |
. . . . . . 7
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑙 ∈ ( L ‘(2nd
‘〈𝐴, 𝐵〉))) → (𝑧 = ((1st
‘〈𝐴, 𝐵〉)( +s ↾ ((((( L
‘𝐴) ∪ ( R
‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))𝑙) ↔ 𝑧 = (𝐴 +s 𝑙))) |
147 | 111, 146 | rexeqbidva 3336 |
. . . . . 6
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (∃𝑙 ∈ ( L ‘(2nd
‘〈𝐴, 𝐵〉))𝑧 = ((1st ‘〈𝐴, 𝐵〉)( +s ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))𝑙) ↔ ∃𝑙 ∈ ( L ‘𝐵)𝑧 = (𝐴 +s 𝑙))) |
148 | 147 | abbidv 2822 |
. . . . 5
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → {𝑧 ∣ ∃𝑙 ∈ ( L ‘(2nd
‘〈𝐴, 𝐵〉))𝑧 = ((1st ‘〈𝐴, 𝐵〉)( +s ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))𝑙)} = {𝑧 ∣ ∃𝑙 ∈ ( L ‘𝐵)𝑧 = (𝐴 +s 𝑙)}) |
149 | 110, 148 | uneq12d 4071 |
. . . 4
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → ({𝑦 ∣ ∃𝑙 ∈ ( L ‘(1st
‘〈𝐴, 𝐵〉))𝑦 = (𝑙( +s ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))(2nd ‘〈𝐴, 𝐵〉))} ∪ {𝑧 ∣ ∃𝑙 ∈ ( L ‘(2nd
‘〈𝐴, 𝐵〉))𝑧 = ((1st ‘〈𝐴, 𝐵〉)( +s ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))𝑙)}) = ({𝑦 ∣ ∃𝑙 ∈ ( L ‘𝐴)𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑙 ∈ ( L ‘𝐵)𝑧 = (𝐴 +s 𝑙)})) |
150 | 69 | fveq2d 6667 |
. . . . . . 7
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → ( R ‘(1st
‘〈𝐴, 𝐵〉)) = ( R ‘𝐴)) |
151 | 150 | eleq2d 2837 |
. . . . . . . . 9
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (𝑟 ∈ ( R ‘(1st
‘〈𝐴, 𝐵〉)) ↔ 𝑟 ∈ ( R ‘𝐴))) |
152 | 72 | adantr 484 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑟 ∈ ( R ‘𝐴)) → (2nd ‘〈𝐴, 𝐵〉) = 𝐵) |
153 | 152 | oveq2d 7172 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑟 ∈ ( R ‘𝐴)) → (𝑟( +s ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))(2nd ‘〈𝐴, 𝐵〉)) = (𝑟( +s ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))𝐵)) |
154 | | elun2 4084 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑟 ∈ ( R ‘𝐴) → 𝑟 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))) |
155 | | elun1 4083 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑟 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴)) → 𝑟 ∈ ((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴})) |
156 | 154, 155 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑟 ∈ ( R ‘𝐴) → 𝑟 ∈ ((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴})) |
157 | 156 | adantl 485 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑟 ∈ ( R ‘𝐴)) → 𝑟 ∈ ((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴})) |
158 | 82 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑟 ∈ ( R ‘𝐴)) → 𝐵 ∈ ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) |
159 | 157, 158 | opelxpd 5566 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑟 ∈ ( R ‘𝐴)) → 〈𝑟, 𝐵〉 ∈ (((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵}))) |
160 | | rightirr 33665 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐴 ∈
No → ¬ 𝐴
∈ ( R ‘𝐴)) |
161 | 160 | adantr 484 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → ¬ 𝐴 ∈ ( R ‘𝐴)) |
162 | | eleq1 2839 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑟 = 𝐴 → (𝑟 ∈ ( R ‘𝐴) ↔ 𝐴 ∈ ( R ‘𝐴))) |
163 | 162 | notbid 321 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑟 = 𝐴 → (¬ 𝑟 ∈ ( R ‘𝐴) ↔ ¬ 𝐴 ∈ ( R ‘𝐴))) |
164 | 161, 163 | syl5ibrcom 250 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (𝑟 = 𝐴 → ¬ 𝑟 ∈ ( R ‘𝐴))) |
165 | 164 | necon2ad 2966 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (𝑟 ∈ ( R ‘𝐴) → 𝑟 ≠ 𝐴)) |
166 | 165 | imp 410 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑟 ∈ ( R ‘𝐴)) → 𝑟 ≠ 𝐴) |
167 | 166 | orcd 870 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑟 ∈ ( R ‘𝐴)) → (𝑟 ≠ 𝐴 ∨ 𝐵 ≠ 𝐵)) |
168 | | simpr 488 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑟 ∈ ( R ‘𝐴)) → 𝑟 ∈ ( R ‘𝐴)) |
169 | | simplr 768 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑟 ∈ ( R ‘𝐴)) → 𝐵 ∈ No
) |
170 | | opthneg 5345 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑟 ∈ ( R ‘𝐴) ∧ 𝐵 ∈ No )
→ (〈𝑟, 𝐵〉 ≠ 〈𝐴, 𝐵〉 ↔ (𝑟 ≠ 𝐴 ∨ 𝐵 ≠ 𝐵))) |
171 | 168, 169,
170 | syl2anc 587 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑟 ∈ ( R ‘𝐴)) → (〈𝑟, 𝐵〉 ≠ 〈𝐴, 𝐵〉 ↔ (𝑟 ≠ 𝐴 ∨ 𝐵 ≠ 𝐵))) |
172 | 167, 171 | mpbird 260 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑟 ∈ ( R ‘𝐴)) → 〈𝑟, 𝐵〉 ≠ 〈𝐴, 𝐵〉) |
173 | | eldifsn 4680 |
. . . . . . . . . . . . . . 15
⊢
(〈𝑟, 𝐵〉 ∈ ((((( L
‘𝐴) ∪ ( R
‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}) ↔ (〈𝑟, 𝐵〉 ∈ (((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∧ 〈𝑟, 𝐵〉 ≠ 〈𝐴, 𝐵〉)) |
174 | 159, 172,
173 | sylanbrc 586 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑟 ∈ ( R ‘𝐴)) → 〈𝑟, 𝐵〉 ∈ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉})) |
175 | 174 | fvresd 6683 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑟 ∈ ( R ‘𝐴)) → (( +s ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))‘〈𝑟, 𝐵〉) = ( +s ‘〈𝑟, 𝐵〉)) |
176 | | df-ov 7159 |
. . . . . . . . . . . . 13
⊢ (𝑟( +s ↾ ((((( L
‘𝐴) ∪ ( R
‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))𝐵) = (( +s ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))‘〈𝑟, 𝐵〉) |
177 | | df-ov 7159 |
. . . . . . . . . . . . 13
⊢ (𝑟 +s 𝐵) = ( +s ‘〈𝑟, 𝐵〉) |
178 | 175, 176,
177 | 3eqtr4g 2818 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑟 ∈ ( R ‘𝐴)) → (𝑟( +s ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))𝐵) = (𝑟 +s 𝐵)) |
179 | 153, 178 | eqtrd 2793 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑟 ∈ ( R ‘𝐴)) → (𝑟( +s ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))(2nd ‘〈𝐴, 𝐵〉)) = (𝑟 +s 𝐵)) |
180 | 179 | eqeq2d 2769 |
. . . . . . . . . 10
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑟 ∈ ( R ‘𝐴)) → (𝑦 = (𝑟( +s ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))(2nd ‘〈𝐴, 𝐵〉)) ↔ 𝑦 = (𝑟 +s 𝐵))) |
181 | 180 | ex 416 |
. . . . . . . . 9
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (𝑟 ∈ ( R ‘𝐴) → (𝑦 = (𝑟( +s ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))(2nd ‘〈𝐴, 𝐵〉)) ↔ 𝑦 = (𝑟 +s 𝐵)))) |
182 | 151, 181 | sylbid 243 |
. . . . . . . 8
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (𝑟 ∈ ( R ‘(1st
‘〈𝐴, 𝐵〉)) → (𝑦 = (𝑟( +s ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))(2nd ‘〈𝐴, 𝐵〉)) ↔ 𝑦 = (𝑟 +s 𝐵)))) |
183 | 182 | imp 410 |
. . . . . . 7
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑟 ∈ ( R ‘(1st
‘〈𝐴, 𝐵〉))) → (𝑦 = (𝑟( +s ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))(2nd ‘〈𝐴, 𝐵〉)) ↔ 𝑦 = (𝑟 +s 𝐵))) |
184 | 150, 183 | rexeqbidva 3336 |
. . . . . 6
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (∃𝑟 ∈ ( R ‘(1st
‘〈𝐴, 𝐵〉))𝑦 = (𝑟( +s ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))(2nd ‘〈𝐴, 𝐵〉)) ↔ ∃𝑟 ∈ ( R ‘𝐴)𝑦 = (𝑟 +s 𝐵))) |
185 | 184 | abbidv 2822 |
. . . . 5
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → {𝑦 ∣ ∃𝑟 ∈ ( R ‘(1st
‘〈𝐴, 𝐵〉))𝑦 = (𝑟( +s ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))(2nd ‘〈𝐴, 𝐵〉))} = {𝑦 ∣ ∃𝑟 ∈ ( R ‘𝐴)𝑦 = (𝑟 +s 𝐵)}) |
186 | 72 | fveq2d 6667 |
. . . . . . 7
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → ( R ‘(2nd
‘〈𝐴, 𝐵〉)) = ( R ‘𝐵)) |
187 | 186 | eleq2d 2837 |
. . . . . . . . 9
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (𝑟 ∈ ( R ‘(2nd
‘〈𝐴, 𝐵〉)) ↔ 𝑟 ∈ ( R ‘𝐵))) |
188 | 69 | adantr 484 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑟 ∈ ( R ‘𝐵)) → (1st ‘〈𝐴, 𝐵〉) = 𝐴) |
189 | 188 | oveq1d 7171 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑟 ∈ ( R ‘𝐵)) → ((1st
‘〈𝐴, 𝐵〉)( +s ↾ ((((( L
‘𝐴) ∪ ( R
‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))𝑟) = (𝐴( +s ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))𝑟)) |
190 | 116 | adantr 484 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑟 ∈ ( R ‘𝐵)) → 𝐴 ∈ {𝐴}) |
191 | 190, 117 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑟 ∈ ( R ‘𝐵)) → 𝐴 ∈ ((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴})) |
192 | | elun2 4084 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑟 ∈ ( R ‘𝐵) → 𝑟 ∈ (( L ‘𝐵) ∪ ( R ‘𝐵))) |
193 | 192 | adantl 485 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑟 ∈ ( R ‘𝐵)) → 𝑟 ∈ (( L ‘𝐵) ∪ ( R ‘𝐵))) |
194 | | elun1 4083 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑟 ∈ (( L ‘𝐵) ∪ ( R ‘𝐵)) → 𝑟 ∈ ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) |
195 | 193, 194 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑟 ∈ ( R ‘𝐵)) → 𝑟 ∈ ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) |
196 | 191, 195 | opelxpd 5566 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑟 ∈ ( R ‘𝐵)) → 〈𝐴, 𝑟〉 ∈ (((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵}))) |
197 | | rightirr 33665 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐵 ∈
No → ¬ 𝐵
∈ ( R ‘𝐵)) |
198 | 197 | adantl 485 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → ¬ 𝐵 ∈ ( R ‘𝐵)) |
199 | | eleq1 2839 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑟 = 𝐵 → (𝑟 ∈ ( R ‘𝐵) ↔ 𝐵 ∈ ( R ‘𝐵))) |
200 | 199 | notbid 321 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑟 = 𝐵 → (¬ 𝑟 ∈ ( R ‘𝐵) ↔ ¬ 𝐵 ∈ ( R ‘𝐵))) |
201 | 198, 200 | syl5ibrcom 250 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (𝑟 = 𝐵 → ¬ 𝑟 ∈ ( R ‘𝐵))) |
202 | 201 | necon2ad 2966 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (𝑟 ∈ ( R ‘𝐵) → 𝑟 ≠ 𝐵)) |
203 | 202 | imp 410 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑟 ∈ ( R ‘𝐵)) → 𝑟 ≠ 𝐵) |
204 | 203 | olcd 871 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑟 ∈ ( R ‘𝐵)) → (𝐴 ≠ 𝐴 ∨ 𝑟 ≠ 𝐵)) |
205 | | opthneg 5345 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈
No ∧ 𝑟 ∈ (
R ‘𝐵)) →
(〈𝐴, 𝑟〉 ≠ 〈𝐴, 𝐵〉 ↔ (𝐴 ≠ 𝐴 ∨ 𝑟 ≠ 𝐵))) |
206 | 205 | adantlr 714 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑟 ∈ ( R ‘𝐵)) → (〈𝐴, 𝑟〉 ≠ 〈𝐴, 𝐵〉 ↔ (𝐴 ≠ 𝐴 ∨ 𝑟 ≠ 𝐵))) |
207 | 204, 206 | mpbird 260 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑟 ∈ ( R ‘𝐵)) → 〈𝐴, 𝑟〉 ≠ 〈𝐴, 𝐵〉) |
208 | | eldifsn 4680 |
. . . . . . . . . . . . . . 15
⊢
(〈𝐴, 𝑟〉 ∈ ((((( L
‘𝐴) ∪ ( R
‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}) ↔ (〈𝐴, 𝑟〉 ∈ (((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∧ 〈𝐴, 𝑟〉 ≠ 〈𝐴, 𝐵〉)) |
209 | 196, 207,
208 | sylanbrc 586 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑟 ∈ ( R ‘𝐵)) → 〈𝐴, 𝑟〉 ∈ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉})) |
210 | 209 | fvresd 6683 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑟 ∈ ( R ‘𝐵)) → (( +s ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))‘〈𝐴, 𝑟〉) = ( +s ‘〈𝐴, 𝑟〉)) |
211 | | df-ov 7159 |
. . . . . . . . . . . . 13
⊢ (𝐴( +s ↾ ((((( L
‘𝐴) ∪ ( R
‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))𝑟) = (( +s ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))‘〈𝐴, 𝑟〉) |
212 | | df-ov 7159 |
. . . . . . . . . . . . 13
⊢ (𝐴 +s 𝑟) = ( +s ‘〈𝐴, 𝑟〉) |
213 | 210, 211,
212 | 3eqtr4g 2818 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑟 ∈ ( R ‘𝐵)) → (𝐴( +s ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))𝑟) = (𝐴 +s 𝑟)) |
214 | 189, 213 | eqtrd 2793 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑟 ∈ ( R ‘𝐵)) → ((1st
‘〈𝐴, 𝐵〉)( +s ↾ ((((( L
‘𝐴) ∪ ( R
‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))𝑟) = (𝐴 +s 𝑟)) |
215 | 214 | eqeq2d 2769 |
. . . . . . . . . 10
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑟 ∈ ( R ‘𝐵)) → (𝑧 = ((1st ‘〈𝐴, 𝐵〉)( +s ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))𝑟) ↔ 𝑧 = (𝐴 +s 𝑟))) |
216 | 215 | ex 416 |
. . . . . . . . 9
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (𝑟 ∈ ( R ‘𝐵) → (𝑧 = ((1st ‘〈𝐴, 𝐵〉)( +s ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))𝑟) ↔ 𝑧 = (𝐴 +s 𝑟)))) |
217 | 187, 216 | sylbid 243 |
. . . . . . . 8
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (𝑟 ∈ ( R ‘(2nd
‘〈𝐴, 𝐵〉)) → (𝑧 = ((1st
‘〈𝐴, 𝐵〉)( +s ↾ ((((( L
‘𝐴) ∪ ( R
‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))𝑟) ↔ 𝑧 = (𝐴 +s 𝑟)))) |
218 | 217 | imp 410 |
. . . . . . 7
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ 𝑟 ∈ ( R ‘(2nd
‘〈𝐴, 𝐵〉))) → (𝑧 = ((1st
‘〈𝐴, 𝐵〉)( +s ↾ ((((( L
‘𝐴) ∪ ( R
‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))𝑟) ↔ 𝑧 = (𝐴 +s 𝑟))) |
219 | 186, 218 | rexeqbidva 3336 |
. . . . . 6
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (∃𝑟 ∈ ( R ‘(2nd
‘〈𝐴, 𝐵〉))𝑧 = ((1st ‘〈𝐴, 𝐵〉)( +s ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))𝑟) ↔ ∃𝑟 ∈ ( R ‘𝐵)𝑧 = (𝐴 +s 𝑟))) |
220 | 219 | abbidv 2822 |
. . . . 5
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → {𝑧 ∣ ∃𝑟 ∈ ( R ‘(2nd
‘〈𝐴, 𝐵〉))𝑧 = ((1st ‘〈𝐴, 𝐵〉)( +s ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))𝑟)} = {𝑧 ∣ ∃𝑟 ∈ ( R ‘𝐵)𝑧 = (𝐴 +s 𝑟)}) |
221 | 185, 220 | uneq12d 4071 |
. . . 4
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → ({𝑦 ∣ ∃𝑟 ∈ ( R ‘(1st
‘〈𝐴, 𝐵〉))𝑦 = (𝑟( +s ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))(2nd ‘〈𝐴, 𝐵〉))} ∪ {𝑧 ∣ ∃𝑟 ∈ ( R ‘(2nd
‘〈𝐴, 𝐵〉))𝑧 = ((1st ‘〈𝐴, 𝐵〉)( +s ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))𝑟)}) = ({𝑦 ∣ ∃𝑟 ∈ ( R ‘𝐴)𝑦 = (𝑟 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑟 ∈ ( R ‘𝐵)𝑧 = (𝐴 +s 𝑟)})) |
222 | 149, 221 | oveq12d 7174 |
. . 3
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (({𝑦 ∣ ∃𝑙 ∈ ( L ‘(1st
‘〈𝐴, 𝐵〉))𝑦 = (𝑙( +s ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))(2nd ‘〈𝐴, 𝐵〉))} ∪ {𝑧 ∣ ∃𝑙 ∈ ( L ‘(2nd
‘〈𝐴, 𝐵〉))𝑧 = ((1st ‘〈𝐴, 𝐵〉)( +s ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))𝑙)}) |s ({𝑦 ∣ ∃𝑟 ∈ ( R ‘(1st
‘〈𝐴, 𝐵〉))𝑦 = (𝑟( +s ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))(2nd ‘〈𝐴, 𝐵〉))} ∪ {𝑧 ∣ ∃𝑟 ∈ ( R ‘(2nd
‘〈𝐴, 𝐵〉))𝑧 = ((1st ‘〈𝐴, 𝐵〉)( +s ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))𝑟)})) = (({𝑦 ∣ ∃𝑙 ∈ ( L ‘𝐴)𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑙 ∈ ( L ‘𝐵)𝑧 = (𝐴 +s 𝑙)}) |s ({𝑦 ∣ ∃𝑟 ∈ ( R ‘𝐴)𝑦 = (𝑟 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑟 ∈ ( R ‘𝐵)𝑧 = (𝐴 +s 𝑟)}))) |
223 | 68, 222 | syl5eq 2805 |
. 2
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (〈𝐴, 𝐵〉(𝑥 ∈ V, 𝑎 ∈ V ↦ (({𝑦 ∣ ∃𝑙 ∈ ( L ‘(1st
‘𝑥))𝑦 = (𝑙𝑎(2nd ‘𝑥))} ∪ {𝑧 ∣ ∃𝑙 ∈ ( L ‘(2nd
‘𝑥))𝑧 = ((1st ‘𝑥)𝑎𝑙)}) |s ({𝑦 ∣ ∃𝑟 ∈ ( R ‘(1st
‘𝑥))𝑦 = (𝑟𝑎(2nd ‘𝑥))} ∪ {𝑧 ∣ ∃𝑟 ∈ ( R ‘(2nd
‘𝑥))𝑧 = ((1st ‘𝑥)𝑎𝑟)})))( +s ↾ ((((( L ‘𝐴) ∪ ( R ‘𝐴)) ∪ {𝐴}) × ((( L ‘𝐵) ∪ ( R ‘𝐵)) ∪ {𝐵})) ∖ {〈𝐴, 𝐵〉}))) = (({𝑦 ∣ ∃𝑙 ∈ ( L ‘𝐴)𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑙 ∈ ( L ‘𝐵)𝑧 = (𝐴 +s 𝑙)}) |s ({𝑦 ∣ ∃𝑟 ∈ ( R ‘𝐴)𝑦 = (𝑟 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑟 ∈ ( R ‘𝐵)𝑧 = (𝐴 +s 𝑟)}))) |
224 | 2, 223 | eqtrd 2793 |
1
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (𝐴 +s 𝐵) = (({𝑦 ∣ ∃𝑙 ∈ ( L ‘𝐴)𝑦 = (𝑙 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑙 ∈ ( L ‘𝐵)𝑧 = (𝐴 +s 𝑙)}) |s ({𝑦 ∣ ∃𝑟 ∈ ( R ‘𝐴)𝑦 = (𝑟 +s 𝐵)} ∪ {𝑧 ∣ ∃𝑟 ∈ ( R ‘𝐵)𝑧 = (𝐴 +s 𝑟)}))) |