Proof of Theorem nosepdmlem
Step | Hyp | Ref
| Expression |
1 | | sltval2 31809 |
. . . . 5
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (𝐴 <s 𝐵 ↔ (𝐴‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}){〈1𝑜,
∅〉, 〈1𝑜, 2𝑜〉,
〈∅, 2𝑜〉} (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}))) |
2 | | fvex 6201 |
. . . . . . 7
⊢ (𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) ∈ V |
3 | | fvex 6201 |
. . . . . . 7
⊢ (𝐵‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) ∈ V |
4 | 2, 3 | brtp 31639 |
. . . . . 6
⊢ ((𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}){〈1𝑜,
∅〉, 〈1𝑜, 2𝑜〉,
〈∅, 2𝑜〉} (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) ↔ (((𝐴‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 1𝑜 ∧ (𝐵‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = ∅) ∨ ((𝐴‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 1𝑜 ∧ (𝐵‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 2𝑜) ∨ ((𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = ∅ ∧ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) =
2𝑜))) |
5 | | df-3or 1038 |
. . . . . . . . . 10
⊢ ((((𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 1𝑜 ∧ (𝐵‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = ∅) ∨ ((𝐴‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 1𝑜 ∧ (𝐵‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 2𝑜) ∨ ((𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = ∅ ∧ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 2𝑜)) ↔
((((𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 1𝑜 ∧ (𝐵‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = ∅) ∨ ((𝐴‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 1𝑜 ∧ (𝐵‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 2𝑜)) ∨ ((𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = ∅ ∧ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) =
2𝑜))) |
6 | | ndmfv 6218 |
. . . . . . . . . . . . 13
⊢ (¬
∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)} ∈ dom 𝐴 → (𝐴‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = ∅) |
7 | | 1on 7567 |
. . . . . . . . . . . . . . . . . . . 20
⊢
1𝑜 ∈ On |
8 | 7 | elexi 3213 |
. . . . . . . . . . . . . . . . . . 19
⊢
1𝑜 ∈ V |
9 | 8 | prid1 4297 |
. . . . . . . . . . . . . . . . . 18
⊢
1𝑜 ∈ {1𝑜,
2𝑜} |
10 | 9 | nosgnn0i 31812 |
. . . . . . . . . . . . . . . . 17
⊢ ∅
≠ 1𝑜 |
11 | | neeq1 2856 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = ∅ → ((𝐴‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) ≠ 1𝑜 ↔ ∅
≠ 1𝑜)) |
12 | 10, 11 | mpbiri 248 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = ∅ → (𝐴‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) ≠
1𝑜) |
13 | 12 | neneqd 2799 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = ∅ → ¬ (𝐴‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 1𝑜) |
14 | 13 | intnanrd 963 |
. . . . . . . . . . . . . 14
⊢ ((𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = ∅ → ¬ ((𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 1𝑜 ∧ (𝐵‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = ∅)) |
15 | 13 | intnanrd 963 |
. . . . . . . . . . . . . 14
⊢ ((𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = ∅ → ¬ ((𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 1𝑜 ∧ (𝐵‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) =
2𝑜)) |
16 | | ioran 511 |
. . . . . . . . . . . . . 14
⊢ (¬
(((𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 1𝑜 ∧ (𝐵‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = ∅) ∨ ((𝐴‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 1𝑜 ∧ (𝐵‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 2𝑜)) ↔ (¬
((𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 1𝑜 ∧ (𝐵‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = ∅) ∧ ¬ ((𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 1𝑜 ∧ (𝐵‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) =
2𝑜))) |
17 | 14, 15, 16 | sylanbrc 698 |
. . . . . . . . . . . . 13
⊢ ((𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = ∅ → ¬ (((𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 1𝑜 ∧ (𝐵‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = ∅) ∨ ((𝐴‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 1𝑜 ∧ (𝐵‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) =
2𝑜))) |
18 | 6, 17 | syl 17 |
. . . . . . . . . . . 12
⊢ (¬
∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)} ∈ dom 𝐴 → ¬ (((𝐴‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 1𝑜 ∧ (𝐵‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = ∅) ∨ ((𝐴‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 1𝑜 ∧ (𝐵‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) =
2𝑜))) |
19 | 18 | adantl 482 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ ¬ ∩
{𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)} ∈ dom 𝐴) → ¬ (((𝐴‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 1𝑜 ∧ (𝐵‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = ∅) ∨ ((𝐴‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 1𝑜 ∧ (𝐵‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) =
2𝑜))) |
20 | | orel1 397 |
. . . . . . . . . . 11
⊢ (¬
(((𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 1𝑜 ∧ (𝐵‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = ∅) ∨ ((𝐴‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 1𝑜 ∧ (𝐵‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 2𝑜)) →
(((((𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 1𝑜 ∧ (𝐵‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = ∅) ∨ ((𝐴‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 1𝑜 ∧ (𝐵‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 2𝑜)) ∨ ((𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = ∅ ∧ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 2𝑜)) → ((𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = ∅ ∧ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) =
2𝑜))) |
21 | 19, 20 | syl 17 |
. . . . . . . . . 10
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ ¬ ∩
{𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)} ∈ dom 𝐴) → (((((𝐴‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 1𝑜 ∧ (𝐵‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = ∅) ∨ ((𝐴‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 1𝑜 ∧ (𝐵‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 2𝑜)) ∨ ((𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = ∅ ∧ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 2𝑜)) → ((𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = ∅ ∧ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) =
2𝑜))) |
22 | 5, 21 | syl5bi 232 |
. . . . . . . . 9
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ ¬ ∩
{𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)} ∈ dom 𝐴) → ((((𝐴‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 1𝑜 ∧ (𝐵‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = ∅) ∨ ((𝐴‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 1𝑜 ∧ (𝐵‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 2𝑜) ∨ ((𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = ∅ ∧ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 2𝑜)) → ((𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = ∅ ∧ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) =
2𝑜))) |
23 | | ndmfv 6218 |
. . . . . . . . . . . . 13
⊢ (¬
∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)} ∈ dom 𝐵 → (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = ∅) |
24 | | 2on 7568 |
. . . . . . . . . . . . . . . . 17
⊢
2𝑜 ∈ On |
25 | 24 | elexi 3213 |
. . . . . . . . . . . . . . . 16
⊢
2𝑜 ∈ V |
26 | 25 | prid2 4298 |
. . . . . . . . . . . . . . 15
⊢
2𝑜 ∈ {1𝑜,
2𝑜} |
27 | 26 | nosgnn0i 31812 |
. . . . . . . . . . . . . 14
⊢ ∅
≠ 2𝑜 |
28 | | neeq1 2856 |
. . . . . . . . . . . . . 14
⊢ ((𝐵‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = ∅ → ((𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) ≠ 2𝑜 ↔ ∅
≠ 2𝑜)) |
29 | 27, 28 | mpbiri 248 |
. . . . . . . . . . . . 13
⊢ ((𝐵‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = ∅ → (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) ≠
2𝑜) |
30 | 23, 29 | syl 17 |
. . . . . . . . . . . 12
⊢ (¬
∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)} ∈ dom 𝐵 → (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) ≠
2𝑜) |
31 | 30 | neneqd 2799 |
. . . . . . . . . . 11
⊢ (¬
∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)} ∈ dom 𝐵 → ¬ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 2𝑜) |
32 | 31 | con4i 113 |
. . . . . . . . . 10
⊢ ((𝐵‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 2𝑜 → ∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)} ∈ dom 𝐵) |
33 | 32 | adantl 482 |
. . . . . . . . 9
⊢ (((𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = ∅ ∧ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 2𝑜) → ∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)} ∈ dom 𝐵) |
34 | 22, 33 | syl6 35 |
. . . . . . . 8
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ ¬ ∩
{𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)} ∈ dom 𝐴) → ((((𝐴‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 1𝑜 ∧ (𝐵‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = ∅) ∨ ((𝐴‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 1𝑜 ∧ (𝐵‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 2𝑜) ∨ ((𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = ∅ ∧ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 2𝑜)) → ∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)} ∈ dom 𝐵)) |
35 | 34 | ex 450 |
. . . . . . 7
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (¬ ∩
{𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)} ∈ dom 𝐴 → ((((𝐴‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 1𝑜 ∧ (𝐵‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = ∅) ∨ ((𝐴‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 1𝑜 ∧ (𝐵‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 2𝑜) ∨ ((𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = ∅ ∧ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 2𝑜)) → ∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)} ∈ dom 𝐵))) |
36 | 35 | com23 86 |
. . . . . 6
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → ((((𝐴‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 1𝑜 ∧ (𝐵‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = ∅) ∨ ((𝐴‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 1𝑜 ∧ (𝐵‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 2𝑜) ∨ ((𝐴‘∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = ∅ ∧ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 2𝑜)) → (¬
∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)} ∈ dom 𝐴 → ∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)} ∈ dom 𝐵))) |
37 | 4, 36 | syl5bi 232 |
. . . . 5
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → ((𝐴‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}){〈1𝑜,
∅〉, 〈1𝑜, 2𝑜〉,
〈∅, 2𝑜〉} (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) → (¬ ∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)} ∈ dom 𝐴 → ∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)} ∈ dom 𝐵))) |
38 | 1, 37 | sylbid 230 |
. . . 4
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (𝐴 <s 𝐵 → (¬ ∩
{𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)} ∈ dom 𝐴 → ∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)} ∈ dom 𝐵))) |
39 | 38 | 3impia 1261 |
. . 3
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ 𝐴 <s 𝐵) → (¬ ∩
{𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)} ∈ dom 𝐴 → ∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)} ∈ dom 𝐵)) |
40 | 39 | orrd 393 |
. 2
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ 𝐴 <s 𝐵) → (∩
{𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)} ∈ dom 𝐴 ∨ ∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)} ∈ dom 𝐵)) |
41 | | elun 3753 |
. 2
⊢ (∩ {𝑥
∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)} ∈ (dom 𝐴 ∪ dom 𝐵) ↔ (∩
{𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)} ∈ dom 𝐴 ∨ ∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)} ∈ dom 𝐵)) |
42 | 40, 41 | sylibr 224 |
1
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ∧ 𝐴 <s 𝐵) → ∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)} ∈ (dom 𝐴 ∪ dom 𝐵)) |