Step | Hyp | Ref
| Expression |
1 | | bnj1523.5 |
. 2
⊢ (𝜑 ↔ (𝑅 FrSe 𝐴 ∧ 𝐻 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐻‘𝑥) = (𝐺‘〈𝑥, (𝐻 ↾ pred(𝑥, 𝐴, 𝑅))〉))) |
2 | | bnj1523.6 |
. . 3
⊢ (𝜓 ↔ (𝜑 ∧ 𝐹 ≠ 𝐻)) |
3 | | bnj1523.9 |
. . . . . . . . . . . . 13
⊢ (𝜃 ↔ (𝜒 ∧ 𝑦 ∈ 𝐷 ∧ ∀𝑧 ∈ 𝐷 ¬ 𝑧𝑅𝑦)) |
4 | | bnj1523.7 |
. . . . . . . . . . . . . 14
⊢ (𝜒 ↔ (𝜓 ∧ 𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) ≠ (𝐻‘𝑥))) |
5 | | bnj1523.1 |
. . . . . . . . . . . . . . . . 17
⊢ 𝐵 = {𝑑 ∣ (𝑑 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝑑 pred(𝑥, 𝐴, 𝑅) ⊆ 𝑑)} |
6 | | bnj1523.2 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑌 = 〈𝑥, (𝑓 ↾ pred(𝑥, 𝐴, 𝑅))〉 |
7 | | bnj1523.3 |
. . . . . . . . . . . . . . . . 17
⊢ 𝐶 = {𝑓 ∣ ∃𝑑 ∈ 𝐵 (𝑓 Fn 𝑑 ∧ ∀𝑥 ∈ 𝑑 (𝑓‘𝑥) = (𝐺‘𝑌))} |
8 | | bnj1523.4 |
. . . . . . . . . . . . . . . . 17
⊢ 𝐹 = ∪
𝐶 |
9 | 5, 6, 7, 8 | bnj60 33028 |
. . . . . . . . . . . . . . . 16
⊢ (𝑅 FrSe 𝐴 → 𝐹 Fn 𝐴) |
10 | 1, 9 | bnj835 32725 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐹 Fn 𝐴) |
11 | 2, 10 | bnj832 32724 |
. . . . . . . . . . . . . 14
⊢ (𝜓 → 𝐹 Fn 𝐴) |
12 | 4, 11 | bnj835 32725 |
. . . . . . . . . . . . 13
⊢ (𝜒 → 𝐹 Fn 𝐴) |
13 | 3, 12 | bnj835 32725 |
. . . . . . . . . . . 12
⊢ (𝜃 → 𝐹 Fn 𝐴) |
14 | 1 | simp2bi 1145 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐻 Fn 𝐴) |
15 | 2, 14 | bnj832 32724 |
. . . . . . . . . . . . . 14
⊢ (𝜓 → 𝐻 Fn 𝐴) |
16 | 4, 15 | bnj835 32725 |
. . . . . . . . . . . . 13
⊢ (𝜒 → 𝐻 Fn 𝐴) |
17 | 3, 16 | bnj835 32725 |
. . . . . . . . . . . 12
⊢ (𝜃 → 𝐻 Fn 𝐴) |
18 | | bnj213 32848 |
. . . . . . . . . . . . 13
⊢
pred(𝑦, 𝐴, 𝑅) ⊆ 𝐴 |
19 | 18 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜃 → pred(𝑦, 𝐴, 𝑅) ⊆ 𝐴) |
20 | 3 | simp3bi 1146 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜃 → ∀𝑧 ∈ 𝐷 ¬ 𝑧𝑅𝑦) |
21 | 20 | bnj1211 32763 |
. . . . . . . . . . . . . . . 16
⊢ (𝜃 → ∀𝑧(𝑧 ∈ 𝐷 → ¬ 𝑧𝑅𝑦)) |
22 | | con2b 360 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑧 ∈ 𝐷 → ¬ 𝑧𝑅𝑦) ↔ (𝑧𝑅𝑦 → ¬ 𝑧 ∈ 𝐷)) |
23 | 22 | albii 1822 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑧(𝑧 ∈ 𝐷 → ¬ 𝑧𝑅𝑦) ↔ ∀𝑧(𝑧𝑅𝑦 → ¬ 𝑧 ∈ 𝐷)) |
24 | 21, 23 | sylib 217 |
. . . . . . . . . . . . . . 15
⊢ (𝜃 → ∀𝑧(𝑧𝑅𝑦 → ¬ 𝑧 ∈ 𝐷)) |
25 | | bnj1418 33006 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈ pred(𝑦, 𝐴, 𝑅) → 𝑧𝑅𝑦) |
26 | 25 | imim1i 63 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑧𝑅𝑦 → ¬ 𝑧 ∈ 𝐷) → (𝑧 ∈ pred(𝑦, 𝐴, 𝑅) → ¬ 𝑧 ∈ 𝐷)) |
27 | 26 | alimi 1814 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑧(𝑧𝑅𝑦 → ¬ 𝑧 ∈ 𝐷) → ∀𝑧(𝑧 ∈ pred(𝑦, 𝐴, 𝑅) → ¬ 𝑧 ∈ 𝐷)) |
28 | 24, 27 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜃 → ∀𝑧(𝑧 ∈ pred(𝑦, 𝐴, 𝑅) → ¬ 𝑧 ∈ 𝐷)) |
29 | 28 | bnj1142 32755 |
. . . . . . . . . . . . 13
⊢ (𝜃 → ∀𝑧 ∈ pred (𝑦, 𝐴, 𝑅) ¬ 𝑧 ∈ 𝐷) |
30 | | bnj1523.8 |
. . . . . . . . . . . . . 14
⊢ 𝐷 = {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) ≠ (𝐻‘𝑥)} |
31 | 5 | bnj1309 32988 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 ∈ 𝐵 → ∀𝑥 𝑤 ∈ 𝐵) |
32 | 7, 31 | bnj1307 32989 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 ∈ 𝐶 → ∀𝑥 𝑤 ∈ 𝐶) |
33 | 32 | nfcii 2891 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑥𝐶 |
34 | 33 | nfuni 4847 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑥∪ 𝐶 |
35 | 8, 34 | nfcxfr 2905 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑥𝐹 |
36 | 35 | nfcrii 2899 |
. . . . . . . . . . . . . 14
⊢ (𝑤 ∈ 𝐹 → ∀𝑥 𝑤 ∈ 𝐹) |
37 | 30, 36 | bnj1534 32819 |
. . . . . . . . . . . . 13
⊢ 𝐷 = {𝑧 ∈ 𝐴 ∣ (𝐹‘𝑧) ≠ (𝐻‘𝑧)} |
38 | 29, 18, 37 | bnj1533 32818 |
. . . . . . . . . . . 12
⊢ (𝜃 → ∀𝑧 ∈ pred (𝑦, 𝐴, 𝑅)(𝐹‘𝑧) = (𝐻‘𝑧)) |
39 | 13, 17, 19, 38 | bnj1536 32820 |
. . . . . . . . . . 11
⊢ (𝜃 → (𝐹 ↾ pred(𝑦, 𝐴, 𝑅)) = (𝐻 ↾ pred(𝑦, 𝐴, 𝑅))) |
40 | 39 | opeq2d 4812 |
. . . . . . . . . 10
⊢ (𝜃 → 〈𝑦, (𝐹 ↾ pred(𝑦, 𝐴, 𝑅))〉 = 〈𝑦, (𝐻 ↾ pred(𝑦, 𝐴, 𝑅))〉) |
41 | 40 | fveq2d 6771 |
. . . . . . . . 9
⊢ (𝜃 → (𝐺‘〈𝑦, (𝐹 ↾ pred(𝑦, 𝐴, 𝑅))〉) = (𝐺‘〈𝑦, (𝐻 ↾ pred(𝑦, 𝐴, 𝑅))〉)) |
42 | 5, 6, 7, 8 | bnj1500 33034 |
. . . . . . . . . . . . . . 15
⊢ (𝑅 FrSe 𝐴 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘〈𝑥, (𝐹 ↾ pred(𝑥, 𝐴, 𝑅))〉)) |
43 | 1, 42 | bnj835 32725 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘〈𝑥, (𝐹 ↾ pred(𝑥, 𝐴, 𝑅))〉)) |
44 | 2, 43 | bnj832 32724 |
. . . . . . . . . . . . 13
⊢ (𝜓 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘〈𝑥, (𝐹 ↾ pred(𝑥, 𝐴, 𝑅))〉)) |
45 | 4, 44 | bnj835 32725 |
. . . . . . . . . . . 12
⊢ (𝜒 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘〈𝑥, (𝐹 ↾ pred(𝑥, 𝐴, 𝑅))〉)) |
46 | 45, 36 | bnj1529 33036 |
. . . . . . . . . . 11
⊢ (𝜒 → ∀𝑦 ∈ 𝐴 (𝐹‘𝑦) = (𝐺‘〈𝑦, (𝐹 ↾ pred(𝑦, 𝐴, 𝑅))〉)) |
47 | 3, 46 | bnj835 32725 |
. . . . . . . . . 10
⊢ (𝜃 → ∀𝑦 ∈ 𝐴 (𝐹‘𝑦) = (𝐺‘〈𝑦, (𝐹 ↾ pred(𝑦, 𝐴, 𝑅))〉)) |
48 | 30 | ssrab3 4015 |
. . . . . . . . . . 11
⊢ 𝐷 ⊆ 𝐴 |
49 | 3 | simp2bi 1145 |
. . . . . . . . . . 11
⊢ (𝜃 → 𝑦 ∈ 𝐷) |
50 | 48, 49 | bnj1213 32764 |
. . . . . . . . . 10
⊢ (𝜃 → 𝑦 ∈ 𝐴) |
51 | 47, 50 | bnj1294 32783 |
. . . . . . . . 9
⊢ (𝜃 → (𝐹‘𝑦) = (𝐺‘〈𝑦, (𝐹 ↾ pred(𝑦, 𝐴, 𝑅))〉)) |
52 | 1 | simp3bi 1146 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝐻‘𝑥) = (𝐺‘〈𝑥, (𝐻 ↾ pred(𝑥, 𝐴, 𝑅))〉)) |
53 | 2, 52 | bnj832 32724 |
. . . . . . . . . . . . 13
⊢ (𝜓 → ∀𝑥 ∈ 𝐴 (𝐻‘𝑥) = (𝐺‘〈𝑥, (𝐻 ↾ pred(𝑥, 𝐴, 𝑅))〉)) |
54 | 4, 53 | bnj835 32725 |
. . . . . . . . . . . 12
⊢ (𝜒 → ∀𝑥 ∈ 𝐴 (𝐻‘𝑥) = (𝐺‘〈𝑥, (𝐻 ↾ pred(𝑥, 𝐴, 𝑅))〉)) |
55 | | ax-5 1913 |
. . . . . . . . . . . 12
⊢ (𝑣 ∈ 𝐻 → ∀𝑥 𝑣 ∈ 𝐻) |
56 | 54, 55 | bnj1529 33036 |
. . . . . . . . . . 11
⊢ (𝜒 → ∀𝑦 ∈ 𝐴 (𝐻‘𝑦) = (𝐺‘〈𝑦, (𝐻 ↾ pred(𝑦, 𝐴, 𝑅))〉)) |
57 | 3, 56 | bnj835 32725 |
. . . . . . . . . 10
⊢ (𝜃 → ∀𝑦 ∈ 𝐴 (𝐻‘𝑦) = (𝐺‘〈𝑦, (𝐻 ↾ pred(𝑦, 𝐴, 𝑅))〉)) |
58 | 57, 50 | bnj1294 32783 |
. . . . . . . . 9
⊢ (𝜃 → (𝐻‘𝑦) = (𝐺‘〈𝑦, (𝐻 ↾ pred(𝑦, 𝐴, 𝑅))〉)) |
59 | 41, 51, 58 | 3eqtr4d 2788 |
. . . . . . . 8
⊢ (𝜃 → (𝐹‘𝑦) = (𝐻‘𝑦)) |
60 | 30, 36 | bnj1534 32819 |
. . . . . . . . . . 11
⊢ 𝐷 = {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) ≠ (𝐻‘𝑦)} |
61 | 60 | bnj1538 32821 |
. . . . . . . . . 10
⊢ (𝑦 ∈ 𝐷 → (𝐹‘𝑦) ≠ (𝐻‘𝑦)) |
62 | 3, 61 | bnj836 32726 |
. . . . . . . . 9
⊢ (𝜃 → (𝐹‘𝑦) ≠ (𝐻‘𝑦)) |
63 | 62 | neneqd 2948 |
. . . . . . . 8
⊢ (𝜃 → ¬ (𝐹‘𝑦) = (𝐻‘𝑦)) |
64 | 59, 63 | pm2.65i 193 |
. . . . . . 7
⊢ ¬
𝜃 |
65 | 64 | nex 1803 |
. . . . . 6
⊢ ¬
∃𝑦𝜃 |
66 | 1 | simp1bi 1144 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑅 FrSe 𝐴) |
67 | 2, 66 | bnj832 32724 |
. . . . . . . . 9
⊢ (𝜓 → 𝑅 FrSe 𝐴) |
68 | 4, 67 | bnj835 32725 |
. . . . . . . 8
⊢ (𝜒 → 𝑅 FrSe 𝐴) |
69 | 48 | a1i 11 |
. . . . . . . 8
⊢ (𝜒 → 𝐷 ⊆ 𝐴) |
70 | 4 | simp2bi 1145 |
. . . . . . . . . 10
⊢ (𝜒 → 𝑥 ∈ 𝐴) |
71 | 4 | simp3bi 1146 |
. . . . . . . . . 10
⊢ (𝜒 → (𝐹‘𝑥) ≠ (𝐻‘𝑥)) |
72 | 30 | rabeq2i 3420 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐷 ↔ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) ≠ (𝐻‘𝑥))) |
73 | 70, 71, 72 | sylanbrc 583 |
. . . . . . . . 9
⊢ (𝜒 → 𝑥 ∈ 𝐷) |
74 | 73 | ne0d 4270 |
. . . . . . . 8
⊢ (𝜒 → 𝐷 ≠ ∅) |
75 | | bnj69 32976 |
. . . . . . . 8
⊢ ((𝑅 FrSe 𝐴 ∧ 𝐷 ⊆ 𝐴 ∧ 𝐷 ≠ ∅) → ∃𝑦 ∈ 𝐷 ∀𝑧 ∈ 𝐷 ¬ 𝑧𝑅𝑦) |
76 | 68, 69, 74, 75 | syl3anc 1370 |
. . . . . . 7
⊢ (𝜒 → ∃𝑦 ∈ 𝐷 ∀𝑧 ∈ 𝐷 ¬ 𝑧𝑅𝑦) |
77 | 76, 3 | bnj1209 32762 |
. . . . . 6
⊢ (𝜒 → ∃𝑦𝜃) |
78 | 65, 77 | mto 196 |
. . . . 5
⊢ ¬
𝜒 |
79 | 78 | nex 1803 |
. . . 4
⊢ ¬
∃𝑥𝜒 |
80 | 2 | simprbi 497 |
. . . . . 6
⊢ (𝜓 → 𝐹 ≠ 𝐻) |
81 | 11, 15, 80, 36 | bnj1542 32823 |
. . . . 5
⊢ (𝜓 → ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) ≠ (𝐻‘𝑥)) |
82 | 5, 6, 7, 8, 1, 2 | bnj1525 33035 |
. . . . 5
⊢ (𝜓 → ∀𝑥𝜓) |
83 | 81, 4, 82 | bnj1521 32817 |
. . . 4
⊢ (𝜓 → ∃𝑥𝜒) |
84 | 79, 83 | mto 196 |
. . 3
⊢ ¬
𝜓 |
85 | 2, 84 | bnj1541 32822 |
. 2
⊢ (𝜑 → 𝐹 = 𝐻) |
86 | 1, 85 | sylbir 234 |
1
⊢ ((𝑅 FrSe 𝐴 ∧ 𝐻 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐻‘𝑥) = (𝐺‘〈𝑥, (𝐻 ↾ pred(𝑥, 𝐴, 𝑅))〉)) → 𝐹 = 𝐻) |