Step | Hyp | Ref
| Expression |
1 | | soseq.1 |
. . . 4
⊢ 𝑅 Or (𝐴 ∪ {∅}) |
2 | | sopo 5492 |
. . . 4
⊢ (𝑅 Or (𝐴 ∪ {∅}) → 𝑅 Po (𝐴 ∪ {∅})) |
3 | 1, 2 | ax-mp 5 |
. . 3
⊢ 𝑅 Po (𝐴 ∪ {∅}) |
4 | | soseq.2 |
. . 3
⊢ 𝐹 = {𝑓 ∣ ∃𝑥 ∈ On 𝑓:𝑥⟶𝐴} |
5 | | soseq.3 |
. . 3
⊢ 𝑆 = {〈𝑓, 𝑔〉 ∣ ((𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)))} |
6 | 3, 4, 5 | poseq 33544 |
. 2
⊢ 𝑆 Po 𝐹 |
7 | | eleq1w 2820 |
. . . . . . . . . . . 12
⊢ (𝑓 = 𝑎 → (𝑓 ∈ 𝐹 ↔ 𝑎 ∈ 𝐹)) |
8 | 7 | anbi1d 633 |
. . . . . . . . . . 11
⊢ (𝑓 = 𝑎 → ((𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ↔ (𝑎 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹))) |
9 | | fveq1 6721 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 = 𝑎 → (𝑓‘𝑦) = (𝑎‘𝑦)) |
10 | 9 | eqeq1d 2739 |
. . . . . . . . . . . . . 14
⊢ (𝑓 = 𝑎 → ((𝑓‘𝑦) = (𝑔‘𝑦) ↔ (𝑎‘𝑦) = (𝑔‘𝑦))) |
11 | 10 | ralbidv 3118 |
. . . . . . . . . . . . 13
⊢ (𝑓 = 𝑎 → (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ↔ ∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑔‘𝑦))) |
12 | | fveq1 6721 |
. . . . . . . . . . . . . 14
⊢ (𝑓 = 𝑎 → (𝑓‘𝑥) = (𝑎‘𝑥)) |
13 | 12 | breq1d 5068 |
. . . . . . . . . . . . 13
⊢ (𝑓 = 𝑎 → ((𝑓‘𝑥)𝑅(𝑔‘𝑥) ↔ (𝑎‘𝑥)𝑅(𝑔‘𝑥))) |
14 | 11, 13 | anbi12d 634 |
. . . . . . . . . . . 12
⊢ (𝑓 = 𝑎 → ((∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)) ↔ (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑔‘𝑥)))) |
15 | 14 | rexbidv 3221 |
. . . . . . . . . . 11
⊢ (𝑓 = 𝑎 → (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)) ↔ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑔‘𝑥)))) |
16 | 8, 15 | anbi12d 634 |
. . . . . . . . . 10
⊢ (𝑓 = 𝑎 → (((𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥))) ↔ ((𝑎 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑔‘𝑥))))) |
17 | | eleq1w 2820 |
. . . . . . . . . . . 12
⊢ (𝑔 = 𝑏 → (𝑔 ∈ 𝐹 ↔ 𝑏 ∈ 𝐹)) |
18 | 17 | anbi2d 632 |
. . . . . . . . . . 11
⊢ (𝑔 = 𝑏 → ((𝑎 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ↔ (𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹))) |
19 | | fveq1 6721 |
. . . . . . . . . . . . . . 15
⊢ (𝑔 = 𝑏 → (𝑔‘𝑦) = (𝑏‘𝑦)) |
20 | 19 | eqeq2d 2748 |
. . . . . . . . . . . . . 14
⊢ (𝑔 = 𝑏 → ((𝑎‘𝑦) = (𝑔‘𝑦) ↔ (𝑎‘𝑦) = (𝑏‘𝑦))) |
21 | 20 | ralbidv 3118 |
. . . . . . . . . . . . 13
⊢ (𝑔 = 𝑏 → (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑔‘𝑦) ↔ ∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦))) |
22 | | fveq1 6721 |
. . . . . . . . . . . . . 14
⊢ (𝑔 = 𝑏 → (𝑔‘𝑥) = (𝑏‘𝑥)) |
23 | 22 | breq2d 5070 |
. . . . . . . . . . . . 13
⊢ (𝑔 = 𝑏 → ((𝑎‘𝑥)𝑅(𝑔‘𝑥) ↔ (𝑎‘𝑥)𝑅(𝑏‘𝑥))) |
24 | 21, 23 | anbi12d 634 |
. . . . . . . . . . . 12
⊢ (𝑔 = 𝑏 → ((∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑔‘𝑥)) ↔ (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑏‘𝑥)))) |
25 | 24 | rexbidv 3221 |
. . . . . . . . . . 11
⊢ (𝑔 = 𝑏 → (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑔‘𝑥)) ↔ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑏‘𝑥)))) |
26 | 18, 25 | anbi12d 634 |
. . . . . . . . . 10
⊢ (𝑔 = 𝑏 → (((𝑎 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑔‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑔‘𝑥))) ↔ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑏‘𝑥))))) |
27 | 16, 26, 5 | brabg 5425 |
. . . . . . . . 9
⊢ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) → (𝑎𝑆𝑏 ↔ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑏‘𝑥))))) |
28 | 27 | bianabs 545 |
. . . . . . . 8
⊢ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) → (𝑎𝑆𝑏 ↔ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑏‘𝑥)))) |
29 | | eleq1w 2820 |
. . . . . . . . . . . . 13
⊢ (𝑓 = 𝑏 → (𝑓 ∈ 𝐹 ↔ 𝑏 ∈ 𝐹)) |
30 | 29 | anbi1d 633 |
. . . . . . . . . . . 12
⊢ (𝑓 = 𝑏 → ((𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ↔ (𝑏 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹))) |
31 | | fveq1 6721 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 = 𝑏 → (𝑓‘𝑦) = (𝑏‘𝑦)) |
32 | 31 | eqeq1d 2739 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 = 𝑏 → ((𝑓‘𝑦) = (𝑔‘𝑦) ↔ (𝑏‘𝑦) = (𝑔‘𝑦))) |
33 | 32 | ralbidv 3118 |
. . . . . . . . . . . . . 14
⊢ (𝑓 = 𝑏 → (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ↔ ∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑔‘𝑦))) |
34 | | fveq1 6721 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 = 𝑏 → (𝑓‘𝑥) = (𝑏‘𝑥)) |
35 | 34 | breq1d 5068 |
. . . . . . . . . . . . . 14
⊢ (𝑓 = 𝑏 → ((𝑓‘𝑥)𝑅(𝑔‘𝑥) ↔ (𝑏‘𝑥)𝑅(𝑔‘𝑥))) |
36 | 33, 35 | anbi12d 634 |
. . . . . . . . . . . . 13
⊢ (𝑓 = 𝑏 → ((∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)) ↔ (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑔‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑔‘𝑥)))) |
37 | 36 | rexbidv 3221 |
. . . . . . . . . . . 12
⊢ (𝑓 = 𝑏 → (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)) ↔ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑔‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑔‘𝑥)))) |
38 | 30, 37 | anbi12d 634 |
. . . . . . . . . . 11
⊢ (𝑓 = 𝑏 → (((𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥))) ↔ ((𝑏 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑔‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑔‘𝑥))))) |
39 | | eleq1w 2820 |
. . . . . . . . . . . . 13
⊢ (𝑔 = 𝑎 → (𝑔 ∈ 𝐹 ↔ 𝑎 ∈ 𝐹)) |
40 | 39 | anbi2d 632 |
. . . . . . . . . . . 12
⊢ (𝑔 = 𝑎 → ((𝑏 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ↔ (𝑏 ∈ 𝐹 ∧ 𝑎 ∈ 𝐹))) |
41 | | fveq1 6721 |
. . . . . . . . . . . . . . . 16
⊢ (𝑔 = 𝑎 → (𝑔‘𝑦) = (𝑎‘𝑦)) |
42 | 41 | eqeq2d 2748 |
. . . . . . . . . . . . . . 15
⊢ (𝑔 = 𝑎 → ((𝑏‘𝑦) = (𝑔‘𝑦) ↔ (𝑏‘𝑦) = (𝑎‘𝑦))) |
43 | 42 | ralbidv 3118 |
. . . . . . . . . . . . . 14
⊢ (𝑔 = 𝑎 → (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑔‘𝑦) ↔ ∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦))) |
44 | | fveq1 6721 |
. . . . . . . . . . . . . . 15
⊢ (𝑔 = 𝑎 → (𝑔‘𝑥) = (𝑎‘𝑥)) |
45 | 44 | breq2d 5070 |
. . . . . . . . . . . . . 14
⊢ (𝑔 = 𝑎 → ((𝑏‘𝑥)𝑅(𝑔‘𝑥) ↔ (𝑏‘𝑥)𝑅(𝑎‘𝑥))) |
46 | 43, 45 | anbi12d 634 |
. . . . . . . . . . . . 13
⊢ (𝑔 = 𝑎 → ((∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑔‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑔‘𝑥)) ↔ (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥)))) |
47 | 46 | rexbidv 3221 |
. . . . . . . . . . . 12
⊢ (𝑔 = 𝑎 → (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑔‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑔‘𝑥)) ↔ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥)))) |
48 | 40, 47 | anbi12d 634 |
. . . . . . . . . . 11
⊢ (𝑔 = 𝑎 → (((𝑏 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑔‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑔‘𝑥))) ↔ ((𝑏 ∈ 𝐹 ∧ 𝑎 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥))))) |
49 | 38, 48, 5 | brabg 5425 |
. . . . . . . . . 10
⊢ ((𝑏 ∈ 𝐹 ∧ 𝑎 ∈ 𝐹) → (𝑏𝑆𝑎 ↔ ((𝑏 ∈ 𝐹 ∧ 𝑎 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥))))) |
50 | 49 | bianabs 545 |
. . . . . . . . 9
⊢ ((𝑏 ∈ 𝐹 ∧ 𝑎 ∈ 𝐹) → (𝑏𝑆𝑎 ↔ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥)))) |
51 | 50 | ancoms 462 |
. . . . . . . 8
⊢ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) → (𝑏𝑆𝑎 ↔ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥)))) |
52 | 28, 51 | orbi12d 919 |
. . . . . . 7
⊢ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) → ((𝑎𝑆𝑏 ∨ 𝑏𝑆𝑎) ↔ (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑏‘𝑥)) ∨ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥))))) |
53 | 52 | notbid 321 |
. . . . . 6
⊢ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) → (¬ (𝑎𝑆𝑏 ∨ 𝑏𝑆𝑎) ↔ ¬ (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑏‘𝑥)) ∨ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥))))) |
54 | | ralinexa 3188 |
. . . . . . . 8
⊢
(∀𝑥 ∈ On
(∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) → ¬ ((𝑎‘𝑥)𝑅(𝑏‘𝑥) ∨ (𝑏‘𝑥)𝑅(𝑎‘𝑥))) ↔ ¬ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ((𝑎‘𝑥)𝑅(𝑏‘𝑥) ∨ (𝑏‘𝑥)𝑅(𝑎‘𝑥)))) |
55 | | andi 1008 |
. . . . . . . . . . 11
⊢
((∀𝑦 ∈
𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ((𝑎‘𝑥)𝑅(𝑏‘𝑥) ∨ (𝑏‘𝑥)𝑅(𝑎‘𝑥))) ↔ ((∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑏‘𝑥)) ∨ (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥)))) |
56 | | eqcom 2744 |
. . . . . . . . . . . . . 14
⊢ ((𝑎‘𝑦) = (𝑏‘𝑦) ↔ (𝑏‘𝑦) = (𝑎‘𝑦)) |
57 | 56 | ralbii 3088 |
. . . . . . . . . . . . 13
⊢
(∀𝑦 ∈
𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ↔ ∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦)) |
58 | 57 | anbi1i 627 |
. . . . . . . . . . . 12
⊢
((∀𝑦 ∈
𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥)) ↔ (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥))) |
59 | 58 | orbi2i 913 |
. . . . . . . . . . 11
⊢
(((∀𝑦 ∈
𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑏‘𝑥)) ∨ (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥))) ↔ ((∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑏‘𝑥)) ∨ (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥)))) |
60 | 55, 59 | bitri 278 |
. . . . . . . . . 10
⊢
((∀𝑦 ∈
𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ((𝑎‘𝑥)𝑅(𝑏‘𝑥) ∨ (𝑏‘𝑥)𝑅(𝑎‘𝑥))) ↔ ((∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑏‘𝑥)) ∨ (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥)))) |
61 | 60 | rexbii 3175 |
. . . . . . . . 9
⊢
(∃𝑥 ∈ On
(∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ((𝑎‘𝑥)𝑅(𝑏‘𝑥) ∨ (𝑏‘𝑥)𝑅(𝑎‘𝑥))) ↔ ∃𝑥 ∈ On ((∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑏‘𝑥)) ∨ (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥)))) |
62 | | r19.43 3269 |
. . . . . . . . 9
⊢
(∃𝑥 ∈ On
((∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑏‘𝑥)) ∨ (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥))) ↔ (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑏‘𝑥)) ∨ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥)))) |
63 | 61, 62 | bitri 278 |
. . . . . . . 8
⊢
(∃𝑥 ∈ On
(∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ ((𝑎‘𝑥)𝑅(𝑏‘𝑥) ∨ (𝑏‘𝑥)𝑅(𝑎‘𝑥))) ↔ (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑏‘𝑥)) ∨ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥)))) |
64 | 54, 63 | xchbinx 337 |
. . . . . . 7
⊢
(∀𝑥 ∈ On
(∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) → ¬ ((𝑎‘𝑥)𝑅(𝑏‘𝑥) ∨ (𝑏‘𝑥)𝑅(𝑎‘𝑥))) ↔ ¬ (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑏‘𝑥)) ∨ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥)))) |
65 | | feq2 6532 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑦 → (𝑓:𝑥⟶𝐴 ↔ 𝑓:𝑦⟶𝐴)) |
66 | 65 | cbvrexvw 3364 |
. . . . . . . . . . . . . 14
⊢
(∃𝑥 ∈ On
𝑓:𝑥⟶𝐴 ↔ ∃𝑦 ∈ On 𝑓:𝑦⟶𝐴) |
67 | 66 | abbii 2808 |
. . . . . . . . . . . . 13
⊢ {𝑓 ∣ ∃𝑥 ∈ On 𝑓:𝑥⟶𝐴} = {𝑓 ∣ ∃𝑦 ∈ On 𝑓:𝑦⟶𝐴} |
68 | 4, 67 | eqtri 2765 |
. . . . . . . . . . . 12
⊢ 𝐹 = {𝑓 ∣ ∃𝑦 ∈ On 𝑓:𝑦⟶𝐴} |
69 | 68 | orderseqlem 33543 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ 𝐹 → (𝑎‘𝑥) ∈ (𝐴 ∪ {∅})) |
70 | 68 | orderseqlem 33543 |
. . . . . . . . . . 11
⊢ (𝑏 ∈ 𝐹 → (𝑏‘𝑥) ∈ (𝐴 ∪ {∅})) |
71 | | sotrieq 5502 |
. . . . . . . . . . . 12
⊢ ((𝑅 Or (𝐴 ∪ {∅}) ∧ ((𝑎‘𝑥) ∈ (𝐴 ∪ {∅}) ∧ (𝑏‘𝑥) ∈ (𝐴 ∪ {∅}))) → ((𝑎‘𝑥) = (𝑏‘𝑥) ↔ ¬ ((𝑎‘𝑥)𝑅(𝑏‘𝑥) ∨ (𝑏‘𝑥)𝑅(𝑎‘𝑥)))) |
72 | 1, 71 | mpan 690 |
. . . . . . . . . . 11
⊢ (((𝑎‘𝑥) ∈ (𝐴 ∪ {∅}) ∧ (𝑏‘𝑥) ∈ (𝐴 ∪ {∅})) → ((𝑎‘𝑥) = (𝑏‘𝑥) ↔ ¬ ((𝑎‘𝑥)𝑅(𝑏‘𝑥) ∨ (𝑏‘𝑥)𝑅(𝑎‘𝑥)))) |
73 | 69, 70, 72 | syl2an 599 |
. . . . . . . . . 10
⊢ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) → ((𝑎‘𝑥) = (𝑏‘𝑥) ↔ ¬ ((𝑎‘𝑥)𝑅(𝑏‘𝑥) ∨ (𝑏‘𝑥)𝑅(𝑎‘𝑥)))) |
74 | 73 | imbi2d 344 |
. . . . . . . . 9
⊢ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) → ((∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) → (𝑎‘𝑥) = (𝑏‘𝑥)) ↔ (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) → ¬ ((𝑎‘𝑥)𝑅(𝑏‘𝑥) ∨ (𝑏‘𝑥)𝑅(𝑎‘𝑥))))) |
75 | 74 | ralbidv 3118 |
. . . . . . . 8
⊢ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) → (∀𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) → (𝑎‘𝑥) = (𝑏‘𝑥)) ↔ ∀𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) → ¬ ((𝑎‘𝑥)𝑅(𝑏‘𝑥) ∨ (𝑏‘𝑥)𝑅(𝑎‘𝑥))))) |
76 | | vex 3417 |
. . . . . . . . . . . . . 14
⊢ 𝑦 ∈ V |
77 | | fveq2 6722 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑦 → (𝑎‘𝑥) = (𝑎‘𝑦)) |
78 | | fveq2 6722 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑦 → (𝑏‘𝑥) = (𝑏‘𝑦)) |
79 | 77, 78 | eqeq12d 2753 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑦 → ((𝑎‘𝑥) = (𝑏‘𝑥) ↔ (𝑎‘𝑦) = (𝑏‘𝑦))) |
80 | 76, 79 | sbcie 3742 |
. . . . . . . . . . . . 13
⊢
([𝑦 / 𝑥](𝑎‘𝑥) = (𝑏‘𝑥) ↔ (𝑎‘𝑦) = (𝑏‘𝑦)) |
81 | 80 | ralbii 3088 |
. . . . . . . . . . . 12
⊢
(∀𝑦 ∈
𝑥 [𝑦 / 𝑥](𝑎‘𝑥) = (𝑏‘𝑥) ↔ ∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦)) |
82 | 81 | imbi1i 353 |
. . . . . . . . . . 11
⊢
((∀𝑦 ∈
𝑥 [𝑦 / 𝑥](𝑎‘𝑥) = (𝑏‘𝑥) → (𝑎‘𝑥) = (𝑏‘𝑥)) ↔ (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) → (𝑎‘𝑥) = (𝑏‘𝑥))) |
83 | 82 | ralbii 3088 |
. . . . . . . . . 10
⊢
(∀𝑥 ∈ On
(∀𝑦 ∈ 𝑥 [𝑦 / 𝑥](𝑎‘𝑥) = (𝑏‘𝑥) → (𝑎‘𝑥) = (𝑏‘𝑥)) ↔ ∀𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) → (𝑎‘𝑥) = (𝑏‘𝑥))) |
84 | | tfisg 33510 |
. . . . . . . . . 10
⊢
(∀𝑥 ∈ On
(∀𝑦 ∈ 𝑥 [𝑦 / 𝑥](𝑎‘𝑥) = (𝑏‘𝑥) → (𝑎‘𝑥) = (𝑏‘𝑥)) → ∀𝑥 ∈ On (𝑎‘𝑥) = (𝑏‘𝑥)) |
85 | 83, 84 | sylbir 238 |
. . . . . . . . 9
⊢
(∀𝑥 ∈ On
(∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) → (𝑎‘𝑥) = (𝑏‘𝑥)) → ∀𝑥 ∈ On (𝑎‘𝑥) = (𝑏‘𝑥)) |
86 | | vex 3417 |
. . . . . . . . . . . . . 14
⊢ 𝑎 ∈ V |
87 | | feq1 6531 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 = 𝑎 → (𝑓:𝑥⟶𝐴 ↔ 𝑎:𝑥⟶𝐴)) |
88 | 87 | rexbidv 3221 |
. . . . . . . . . . . . . 14
⊢ (𝑓 = 𝑎 → (∃𝑥 ∈ On 𝑓:𝑥⟶𝐴 ↔ ∃𝑥 ∈ On 𝑎:𝑥⟶𝐴)) |
89 | 86, 88, 4 | elab2 3596 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ 𝐹 ↔ ∃𝑥 ∈ On 𝑎:𝑥⟶𝐴) |
90 | | feq2 6532 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑝 → (𝑎:𝑥⟶𝐴 ↔ 𝑎:𝑝⟶𝐴)) |
91 | 90 | cbvrexvw 3364 |
. . . . . . . . . . . . 13
⊢
(∃𝑥 ∈ On
𝑎:𝑥⟶𝐴 ↔ ∃𝑝 ∈ On 𝑎:𝑝⟶𝐴) |
92 | 89, 91 | bitri 278 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ 𝐹 ↔ ∃𝑝 ∈ On 𝑎:𝑝⟶𝐴) |
93 | | vex 3417 |
. . . . . . . . . . . . . 14
⊢ 𝑏 ∈ V |
94 | | feq1 6531 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 = 𝑏 → (𝑓:𝑥⟶𝐴 ↔ 𝑏:𝑥⟶𝐴)) |
95 | 94 | rexbidv 3221 |
. . . . . . . . . . . . . 14
⊢ (𝑓 = 𝑏 → (∃𝑥 ∈ On 𝑓:𝑥⟶𝐴 ↔ ∃𝑥 ∈ On 𝑏:𝑥⟶𝐴)) |
96 | 93, 95, 4 | elab2 3596 |
. . . . . . . . . . . . 13
⊢ (𝑏 ∈ 𝐹 ↔ ∃𝑥 ∈ On 𝑏:𝑥⟶𝐴) |
97 | | feq2 6532 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑞 → (𝑏:𝑥⟶𝐴 ↔ 𝑏:𝑞⟶𝐴)) |
98 | 97 | cbvrexvw 3364 |
. . . . . . . . . . . . 13
⊢
(∃𝑥 ∈ On
𝑏:𝑥⟶𝐴 ↔ ∃𝑞 ∈ On 𝑏:𝑞⟶𝐴) |
99 | 96, 98 | bitri 278 |
. . . . . . . . . . . 12
⊢ (𝑏 ∈ 𝐹 ↔ ∃𝑞 ∈ On 𝑏:𝑞⟶𝐴) |
100 | 92, 99 | anbi12i 630 |
. . . . . . . . . . 11
⊢ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ↔ (∃𝑝 ∈ On 𝑎:𝑝⟶𝐴 ∧ ∃𝑞 ∈ On 𝑏:𝑞⟶𝐴)) |
101 | | reeanv 3284 |
. . . . . . . . . . 11
⊢
(∃𝑝 ∈ On
∃𝑞 ∈ On (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴) ↔ (∃𝑝 ∈ On 𝑎:𝑝⟶𝐴 ∧ ∃𝑞 ∈ On 𝑏:𝑞⟶𝐴)) |
102 | 100, 101 | bitr4i 281 |
. . . . . . . . . 10
⊢ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) ↔ ∃𝑝 ∈ On ∃𝑞 ∈ On (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) |
103 | | onss 7573 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑞 ∈ On → 𝑞 ⊆ On) |
104 | | ssralv 3972 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑞 ⊆ On →
(∀𝑥 ∈ On (𝑎‘𝑥) = (𝑏‘𝑥) → ∀𝑥 ∈ 𝑞 (𝑎‘𝑥) = (𝑏‘𝑥))) |
105 | 103, 104 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑞 ∈ On → (∀𝑥 ∈ On (𝑎‘𝑥) = (𝑏‘𝑥) → ∀𝑥 ∈ 𝑞 (𝑎‘𝑥) = (𝑏‘𝑥))) |
106 | 105 | ad2antlr 727 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (∀𝑥 ∈ On (𝑎‘𝑥) = (𝑏‘𝑥) → ∀𝑥 ∈ 𝑞 (𝑎‘𝑥) = (𝑏‘𝑥))) |
107 | | soseq.4 |
. . . . . . . . . . . . . . . . . . 19
⊢ ¬
∅ ∈ 𝐴 |
108 | | fveq2 6722 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 = 𝑝 → (𝑎‘𝑥) = (𝑎‘𝑝)) |
109 | | fveq2 6722 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 = 𝑝 → (𝑏‘𝑥) = (𝑏‘𝑝)) |
110 | 108, 109 | eqeq12d 2753 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 = 𝑝 → ((𝑎‘𝑥) = (𝑏‘𝑥) ↔ (𝑎‘𝑝) = (𝑏‘𝑝))) |
111 | 110 | rspcv 3537 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑝 ∈ 𝑞 → (∀𝑥 ∈ 𝑞 (𝑎‘𝑥) = (𝑏‘𝑥) → (𝑎‘𝑝) = (𝑏‘𝑝))) |
112 | 111 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (𝑝 ∈ 𝑞 → (∀𝑥 ∈ 𝑞 (𝑎‘𝑥) = (𝑏‘𝑥) → (𝑎‘𝑝) = (𝑏‘𝑝)))) |
113 | | ffvelrn 6907 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑏:𝑞⟶𝐴 ∧ 𝑝 ∈ 𝑞) → (𝑏‘𝑝) ∈ 𝐴) |
114 | | fdm 6559 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑎:𝑝⟶𝐴 → dom 𝑎 = 𝑝) |
115 | | eloni 6228 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑝 ∈ On → Ord 𝑝) |
116 | | ordirr 6236 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (Ord
𝑝 → ¬ 𝑝 ∈ 𝑝) |
117 | 115, 116 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑝 ∈ On → ¬ 𝑝 ∈ 𝑝) |
118 | | eleq2 2826 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (dom
𝑎 = 𝑝 → (𝑝 ∈ dom 𝑎 ↔ 𝑝 ∈ 𝑝)) |
119 | 118 | notbid 321 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (dom
𝑎 = 𝑝 → (¬ 𝑝 ∈ dom 𝑎 ↔ ¬ 𝑝 ∈ 𝑝)) |
120 | 119 | biimparc 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((¬
𝑝 ∈ 𝑝 ∧ dom 𝑎 = 𝑝) → ¬ 𝑝 ∈ dom 𝑎) |
121 | 117, 120 | sylan 583 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑝 ∈ On ∧ dom 𝑎 = 𝑝) → ¬ 𝑝 ∈ dom 𝑎) |
122 | | ndmfv 6752 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (¬
𝑝 ∈ dom 𝑎 → (𝑎‘𝑝) = ∅) |
123 | | eqtr2 2761 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝑎‘𝑝) = ∅ ∧ (𝑎‘𝑝) = (𝑏‘𝑝)) → ∅ = (𝑏‘𝑝)) |
124 | | eleq1 2825 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (∅
= (𝑏‘𝑝) → (∅ ∈ 𝐴 ↔ (𝑏‘𝑝) ∈ 𝐴)) |
125 | 124 | biimprd 251 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (∅
= (𝑏‘𝑝) → ((𝑏‘𝑝) ∈ 𝐴 → ∅ ∈ 𝐴)) |
126 | 123, 125 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝑎‘𝑝) = ∅ ∧ (𝑎‘𝑝) = (𝑏‘𝑝)) → ((𝑏‘𝑝) ∈ 𝐴 → ∅ ∈ 𝐴)) |
127 | 126 | ex 416 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑎‘𝑝) = ∅ → ((𝑎‘𝑝) = (𝑏‘𝑝) → ((𝑏‘𝑝) ∈ 𝐴 → ∅ ∈ 𝐴))) |
128 | 121, 122,
127 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑝 ∈ On ∧ dom 𝑎 = 𝑝) → ((𝑎‘𝑝) = (𝑏‘𝑝) → ((𝑏‘𝑝) ∈ 𝐴 → ∅ ∈ 𝐴))) |
129 | 128 | com23 86 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑝 ∈ On ∧ dom 𝑎 = 𝑝) → ((𝑏‘𝑝) ∈ 𝐴 → ((𝑎‘𝑝) = (𝑏‘𝑝) → ∅ ∈ 𝐴))) |
130 | 114, 129 | sylan2 596 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑝 ∈ On ∧ 𝑎:𝑝⟶𝐴) → ((𝑏‘𝑝) ∈ 𝐴 → ((𝑎‘𝑝) = (𝑏‘𝑝) → ∅ ∈ 𝐴))) |
131 | 130 | adantlr 715 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ 𝑎:𝑝⟶𝐴) → ((𝑏‘𝑝) ∈ 𝐴 → ((𝑎‘𝑝) = (𝑏‘𝑝) → ∅ ∈ 𝐴))) |
132 | 113, 131 | syl5 34 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ 𝑎:𝑝⟶𝐴) → ((𝑏:𝑞⟶𝐴 ∧ 𝑝 ∈ 𝑞) → ((𝑎‘𝑝) = (𝑏‘𝑝) → ∅ ∈ 𝐴))) |
133 | 132 | exp4b 434 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑝 ∈ On ∧ 𝑞 ∈ On) → (𝑎:𝑝⟶𝐴 → (𝑏:𝑞⟶𝐴 → (𝑝 ∈ 𝑞 → ((𝑎‘𝑝) = (𝑏‘𝑝) → ∅ ∈ 𝐴))))) |
134 | 133 | imp32 422 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (𝑝 ∈ 𝑞 → ((𝑎‘𝑝) = (𝑏‘𝑝) → ∅ ∈ 𝐴))) |
135 | 112, 134 | syldd 72 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (𝑝 ∈ 𝑞 → (∀𝑥 ∈ 𝑞 (𝑎‘𝑥) = (𝑏‘𝑥) → ∅ ∈ 𝐴))) |
136 | 135 | com23 86 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (∀𝑥 ∈ 𝑞 (𝑎‘𝑥) = (𝑏‘𝑥) → (𝑝 ∈ 𝑞 → ∅ ∈ 𝐴))) |
137 | 136 | imp 410 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) ∧ ∀𝑥 ∈ 𝑞 (𝑎‘𝑥) = (𝑏‘𝑥)) → (𝑝 ∈ 𝑞 → ∅ ∈ 𝐴)) |
138 | 107, 137 | mtoi 202 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) ∧ ∀𝑥 ∈ 𝑞 (𝑎‘𝑥) = (𝑏‘𝑥)) → ¬ 𝑝 ∈ 𝑞) |
139 | 138 | ex 416 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (∀𝑥 ∈ 𝑞 (𝑎‘𝑥) = (𝑏‘𝑥) → ¬ 𝑝 ∈ 𝑞)) |
140 | 106, 139 | syld 47 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (∀𝑥 ∈ On (𝑎‘𝑥) = (𝑏‘𝑥) → ¬ 𝑝 ∈ 𝑞)) |
141 | | onss 7573 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑝 ∈ On → 𝑝 ⊆ On) |
142 | | ssralv 3972 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑝 ⊆ On →
(∀𝑥 ∈ On (𝑎‘𝑥) = (𝑏‘𝑥) → ∀𝑥 ∈ 𝑝 (𝑎‘𝑥) = (𝑏‘𝑥))) |
143 | 141, 142 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑝 ∈ On → (∀𝑥 ∈ On (𝑎‘𝑥) = (𝑏‘𝑥) → ∀𝑥 ∈ 𝑝 (𝑎‘𝑥) = (𝑏‘𝑥))) |
144 | 143 | ad2antrr 726 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (∀𝑥 ∈ On (𝑎‘𝑥) = (𝑏‘𝑥) → ∀𝑥 ∈ 𝑝 (𝑎‘𝑥) = (𝑏‘𝑥))) |
145 | | fveq2 6722 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 = 𝑞 → (𝑎‘𝑥) = (𝑎‘𝑞)) |
146 | | fveq2 6722 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 = 𝑞 → (𝑏‘𝑥) = (𝑏‘𝑞)) |
147 | 145, 146 | eqeq12d 2753 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 = 𝑞 → ((𝑎‘𝑥) = (𝑏‘𝑥) ↔ (𝑎‘𝑞) = (𝑏‘𝑞))) |
148 | 147 | rspcv 3537 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑞 ∈ 𝑝 → (∀𝑥 ∈ 𝑝 (𝑎‘𝑥) = (𝑏‘𝑥) → (𝑎‘𝑞) = (𝑏‘𝑞))) |
149 | 148 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (𝑞 ∈ 𝑝 → (∀𝑥 ∈ 𝑝 (𝑎‘𝑥) = (𝑏‘𝑥) → (𝑎‘𝑞) = (𝑏‘𝑞)))) |
150 | | ffvelrn 6907 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑎:𝑝⟶𝐴 ∧ 𝑞 ∈ 𝑝) → (𝑎‘𝑞) ∈ 𝐴) |
151 | | fdm 6559 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑏:𝑞⟶𝐴 → dom 𝑏 = 𝑞) |
152 | | eloni 6228 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑞 ∈ On → Ord 𝑞) |
153 | | ordirr 6236 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (Ord
𝑞 → ¬ 𝑞 ∈ 𝑞) |
154 | 152, 153 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑞 ∈ On → ¬ 𝑞 ∈ 𝑞) |
155 | | eleq2 2826 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (dom
𝑏 = 𝑞 → (𝑞 ∈ dom 𝑏 ↔ 𝑞 ∈ 𝑞)) |
156 | 155 | notbid 321 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (dom
𝑏 = 𝑞 → (¬ 𝑞 ∈ dom 𝑏 ↔ ¬ 𝑞 ∈ 𝑞)) |
157 | 156 | biimparc 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((¬
𝑞 ∈ 𝑞 ∧ dom 𝑏 = 𝑞) → ¬ 𝑞 ∈ dom 𝑏) |
158 | | ndmfv 6752 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (¬
𝑞 ∈ dom 𝑏 → (𝑏‘𝑞) = ∅) |
159 | 157, 158 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((¬
𝑞 ∈ 𝑞 ∧ dom 𝑏 = 𝑞) → (𝑏‘𝑞) = ∅) |
160 | 154, 159 | sylan 583 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑞 ∈ On ∧ dom 𝑏 = 𝑞) → (𝑏‘𝑞) = ∅) |
161 | | eqtr 2760 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝑎‘𝑞) = (𝑏‘𝑞) ∧ (𝑏‘𝑞) = ∅) → (𝑎‘𝑞) = ∅) |
162 | | eleq1 2825 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑎‘𝑞) = ∅ → ((𝑎‘𝑞) ∈ 𝐴 ↔ ∅ ∈ 𝐴)) |
163 | 162 | biimpd 232 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑎‘𝑞) = ∅ → ((𝑎‘𝑞) ∈ 𝐴 → ∅ ∈ 𝐴)) |
164 | 161, 163 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝑎‘𝑞) = (𝑏‘𝑞) ∧ (𝑏‘𝑞) = ∅) → ((𝑎‘𝑞) ∈ 𝐴 → ∅ ∈ 𝐴)) |
165 | 164 | expcom 417 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑏‘𝑞) = ∅ → ((𝑎‘𝑞) = (𝑏‘𝑞) → ((𝑎‘𝑞) ∈ 𝐴 → ∅ ∈ 𝐴))) |
166 | 165 | com23 86 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑏‘𝑞) = ∅ → ((𝑎‘𝑞) ∈ 𝐴 → ((𝑎‘𝑞) = (𝑏‘𝑞) → ∅ ∈ 𝐴))) |
167 | 160, 166 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑞 ∈ On ∧ dom 𝑏 = 𝑞) → ((𝑎‘𝑞) ∈ 𝐴 → ((𝑎‘𝑞) = (𝑏‘𝑞) → ∅ ∈ 𝐴))) |
168 | 167 | adantll 714 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ dom 𝑏 = 𝑞) → ((𝑎‘𝑞) ∈ 𝐴 → ((𝑎‘𝑞) = (𝑏‘𝑞) → ∅ ∈ 𝐴))) |
169 | 151, 168 | sylan2 596 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ 𝑏:𝑞⟶𝐴) → ((𝑎‘𝑞) ∈ 𝐴 → ((𝑎‘𝑞) = (𝑏‘𝑞) → ∅ ∈ 𝐴))) |
170 | 150, 169 | syl5 34 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ 𝑏:𝑞⟶𝐴) → ((𝑎:𝑝⟶𝐴 ∧ 𝑞 ∈ 𝑝) → ((𝑎‘𝑞) = (𝑏‘𝑞) → ∅ ∈ 𝐴))) |
171 | 170 | exp4b 434 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑝 ∈ On ∧ 𝑞 ∈ On) → (𝑏:𝑞⟶𝐴 → (𝑎:𝑝⟶𝐴 → (𝑞 ∈ 𝑝 → ((𝑎‘𝑞) = (𝑏‘𝑞) → ∅ ∈ 𝐴))))) |
172 | 171 | com23 86 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑝 ∈ On ∧ 𝑞 ∈ On) → (𝑎:𝑝⟶𝐴 → (𝑏:𝑞⟶𝐴 → (𝑞 ∈ 𝑝 → ((𝑎‘𝑞) = (𝑏‘𝑞) → ∅ ∈ 𝐴))))) |
173 | 172 | imp32 422 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (𝑞 ∈ 𝑝 → ((𝑎‘𝑞) = (𝑏‘𝑞) → ∅ ∈ 𝐴))) |
174 | 149, 173 | syldd 72 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (𝑞 ∈ 𝑝 → (∀𝑥 ∈ 𝑝 (𝑎‘𝑥) = (𝑏‘𝑥) → ∅ ∈ 𝐴))) |
175 | 174 | com23 86 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (∀𝑥 ∈ 𝑝 (𝑎‘𝑥) = (𝑏‘𝑥) → (𝑞 ∈ 𝑝 → ∅ ∈ 𝐴))) |
176 | 175 | imp 410 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) ∧ ∀𝑥 ∈ 𝑝 (𝑎‘𝑥) = (𝑏‘𝑥)) → (𝑞 ∈ 𝑝 → ∅ ∈ 𝐴)) |
177 | 107, 176 | mtoi 202 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) ∧ ∀𝑥 ∈ 𝑝 (𝑎‘𝑥) = (𝑏‘𝑥)) → ¬ 𝑞 ∈ 𝑝) |
178 | 177 | ex 416 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (∀𝑥 ∈ 𝑝 (𝑎‘𝑥) = (𝑏‘𝑥) → ¬ 𝑞 ∈ 𝑝)) |
179 | 144, 178 | syld 47 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (∀𝑥 ∈ On (𝑎‘𝑥) = (𝑏‘𝑥) → ¬ 𝑞 ∈ 𝑝)) |
180 | 140, 179 | jcad 516 |
. . . . . . . . . . . . . . 15
⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (∀𝑥 ∈ On (𝑎‘𝑥) = (𝑏‘𝑥) → (¬ 𝑝 ∈ 𝑞 ∧ ¬ 𝑞 ∈ 𝑝))) |
181 | | ordtri3or 6250 |
. . . . . . . . . . . . . . . . 17
⊢ ((Ord
𝑝 ∧ Ord 𝑞) → (𝑝 ∈ 𝑞 ∨ 𝑝 = 𝑞 ∨ 𝑞 ∈ 𝑝)) |
182 | 115, 152,
181 | syl2an 599 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑝 ∈ On ∧ 𝑞 ∈ On) → (𝑝 ∈ 𝑞 ∨ 𝑝 = 𝑞 ∨ 𝑞 ∈ 𝑝)) |
183 | 182 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (𝑝 ∈ 𝑞 ∨ 𝑝 = 𝑞 ∨ 𝑞 ∈ 𝑝)) |
184 | | 3orel13 33380 |
. . . . . . . . . . . . . . 15
⊢ ((¬
𝑝 ∈ 𝑞 ∧ ¬ 𝑞 ∈ 𝑝) → ((𝑝 ∈ 𝑞 ∨ 𝑝 = 𝑞 ∨ 𝑞 ∈ 𝑝) → 𝑝 = 𝑞)) |
185 | 180, 183,
184 | syl6ci 71 |
. . . . . . . . . . . . . 14
⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (∀𝑥 ∈ On (𝑎‘𝑥) = (𝑏‘𝑥) → 𝑝 = 𝑞)) |
186 | 185, 144 | jcad 516 |
. . . . . . . . . . . . 13
⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (∀𝑥 ∈ On (𝑎‘𝑥) = (𝑏‘𝑥) → (𝑝 = 𝑞 ∧ ∀𝑥 ∈ 𝑝 (𝑎‘𝑥) = (𝑏‘𝑥)))) |
187 | | ffn 6550 |
. . . . . . . . . . . . . . 15
⊢ (𝑎:𝑝⟶𝐴 → 𝑎 Fn 𝑝) |
188 | | ffn 6550 |
. . . . . . . . . . . . . . 15
⊢ (𝑏:𝑞⟶𝐴 → 𝑏 Fn 𝑞) |
189 | | eqfnfv2 6858 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 Fn 𝑝 ∧ 𝑏 Fn 𝑞) → (𝑎 = 𝑏 ↔ (𝑝 = 𝑞 ∧ ∀𝑥 ∈ 𝑝 (𝑎‘𝑥) = (𝑏‘𝑥)))) |
190 | 187, 188,
189 | syl2an 599 |
. . . . . . . . . . . . . 14
⊢ ((𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴) → (𝑎 = 𝑏 ↔ (𝑝 = 𝑞 ∧ ∀𝑥 ∈ 𝑝 (𝑎‘𝑥) = (𝑏‘𝑥)))) |
191 | 190 | adantl 485 |
. . . . . . . . . . . . 13
⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (𝑎 = 𝑏 ↔ (𝑝 = 𝑞 ∧ ∀𝑥 ∈ 𝑝 (𝑎‘𝑥) = (𝑏‘𝑥)))) |
192 | 186, 191 | sylibrd 262 |
. . . . . . . . . . . 12
⊢ (((𝑝 ∈ On ∧ 𝑞 ∈ On) ∧ (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴)) → (∀𝑥 ∈ On (𝑎‘𝑥) = (𝑏‘𝑥) → 𝑎 = 𝑏)) |
193 | 192 | ex 416 |
. . . . . . . . . . 11
⊢ ((𝑝 ∈ On ∧ 𝑞 ∈ On) → ((𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴) → (∀𝑥 ∈ On (𝑎‘𝑥) = (𝑏‘𝑥) → 𝑎 = 𝑏))) |
194 | 193 | rexlimivv 3216 |
. . . . . . . . . 10
⊢
(∃𝑝 ∈ On
∃𝑞 ∈ On (𝑎:𝑝⟶𝐴 ∧ 𝑏:𝑞⟶𝐴) → (∀𝑥 ∈ On (𝑎‘𝑥) = (𝑏‘𝑥) → 𝑎 = 𝑏)) |
195 | 102, 194 | sylbi 220 |
. . . . . . . . 9
⊢ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) → (∀𝑥 ∈ On (𝑎‘𝑥) = (𝑏‘𝑥) → 𝑎 = 𝑏)) |
196 | 85, 195 | syl5 34 |
. . . . . . . 8
⊢ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) → (∀𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) → (𝑎‘𝑥) = (𝑏‘𝑥)) → 𝑎 = 𝑏)) |
197 | 75, 196 | sylbird 263 |
. . . . . . 7
⊢ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) → (∀𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) → ¬ ((𝑎‘𝑥)𝑅(𝑏‘𝑥) ∨ (𝑏‘𝑥)𝑅(𝑎‘𝑥))) → 𝑎 = 𝑏)) |
198 | 64, 197 | syl5bir 246 |
. . . . . 6
⊢ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) → (¬ (∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑎‘𝑦) = (𝑏‘𝑦) ∧ (𝑎‘𝑥)𝑅(𝑏‘𝑥)) ∨ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑏‘𝑦) = (𝑎‘𝑦) ∧ (𝑏‘𝑥)𝑅(𝑎‘𝑥))) → 𝑎 = 𝑏)) |
199 | 53, 198 | sylbid 243 |
. . . . 5
⊢ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) → (¬ (𝑎𝑆𝑏 ∨ 𝑏𝑆𝑎) → 𝑎 = 𝑏)) |
200 | 199 | orrd 863 |
. . . 4
⊢ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) → ((𝑎𝑆𝑏 ∨ 𝑏𝑆𝑎) ∨ 𝑎 = 𝑏)) |
201 | | 3orcomb 1096 |
. . . . 5
⊢ ((𝑎𝑆𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏𝑆𝑎) ↔ (𝑎𝑆𝑏 ∨ 𝑏𝑆𝑎 ∨ 𝑎 = 𝑏)) |
202 | | df-3or 1090 |
. . . . 5
⊢ ((𝑎𝑆𝑏 ∨ 𝑏𝑆𝑎 ∨ 𝑎 = 𝑏) ↔ ((𝑎𝑆𝑏 ∨ 𝑏𝑆𝑎) ∨ 𝑎 = 𝑏)) |
203 | 201, 202 | bitr2i 279 |
. . . 4
⊢ (((𝑎𝑆𝑏 ∨ 𝑏𝑆𝑎) ∨ 𝑎 = 𝑏) ↔ (𝑎𝑆𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏𝑆𝑎)) |
204 | 200, 203 | sylib 221 |
. . 3
⊢ ((𝑎 ∈ 𝐹 ∧ 𝑏 ∈ 𝐹) → (𝑎𝑆𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏𝑆𝑎)) |
205 | 204 | rgen2 3124 |
. 2
⊢
∀𝑎 ∈
𝐹 ∀𝑏 ∈ 𝐹 (𝑎𝑆𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏𝑆𝑎) |
206 | | df-so 5474 |
. 2
⊢ (𝑆 Or 𝐹 ↔ (𝑆 Po 𝐹 ∧ ∀𝑎 ∈ 𝐹 ∀𝑏 ∈ 𝐹 (𝑎𝑆𝑏 ∨ 𝑎 = 𝑏 ∨ 𝑏𝑆𝑎))) |
207 | 6, 205, 206 | mpbir2an 711 |
1
⊢ 𝑆 Or 𝐹 |