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 31130 |
. . . . . . . . . . . . . . . 16
⊢ (𝑅 FrSe 𝐴 → 𝐹 Fn 𝐴) |
10 | 1, 9 | bnj835 30829 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐹 Fn 𝐴) |
11 | 2, 10 | bnj832 30828 |
. . . . . . . . . . . . . 14
⊢ (𝜓 → 𝐹 Fn 𝐴) |
12 | 4, 11 | bnj835 30829 |
. . . . . . . . . . . . 13
⊢ (𝜒 → 𝐹 Fn 𝐴) |
13 | 3, 12 | bnj835 30829 |
. . . . . . . . . . . 12
⊢ (𝜃 → 𝐹 Fn 𝐴) |
14 | 1 | simp2bi 1077 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐻 Fn 𝐴) |
15 | 2, 14 | bnj832 30828 |
. . . . . . . . . . . . . 14
⊢ (𝜓 → 𝐻 Fn 𝐴) |
16 | 4, 15 | bnj835 30829 |
. . . . . . . . . . . . 13
⊢ (𝜒 → 𝐻 Fn 𝐴) |
17 | 3, 16 | bnj835 30829 |
. . . . . . . . . . . 12
⊢ (𝜃 → 𝐻 Fn 𝐴) |
18 | | bnj213 30952 |
. . . . . . . . . . . . 13
⊢
pred(𝑦, 𝐴, 𝑅) ⊆ 𝐴 |
19 | 18 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜃 → pred(𝑦, 𝐴, 𝑅) ⊆ 𝐴) |
20 | 3 | simp3bi 1078 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜃 → ∀𝑧 ∈ 𝐷 ¬ 𝑧𝑅𝑦) |
21 | 20 | bnj1211 30868 |
. . . . . . . . . . . . . . . 16
⊢ (𝜃 → ∀𝑧(𝑧 ∈ 𝐷 → ¬ 𝑧𝑅𝑦)) |
22 | | con2b 349 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑧 ∈ 𝐷 → ¬ 𝑧𝑅𝑦) ↔ (𝑧𝑅𝑦 → ¬ 𝑧 ∈ 𝐷)) |
23 | 22 | albii 1747 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑧(𝑧 ∈ 𝐷 → ¬ 𝑧𝑅𝑦) ↔ ∀𝑧(𝑧𝑅𝑦 → ¬ 𝑧 ∈ 𝐷)) |
24 | 21, 23 | sylib 208 |
. . . . . . . . . . . . . . 15
⊢ (𝜃 → ∀𝑧(𝑧𝑅𝑦 → ¬ 𝑧 ∈ 𝐷)) |
25 | | bnj1418 31108 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈ pred(𝑦, 𝐴, 𝑅) → 𝑧𝑅𝑦) |
26 | 25 | imim1i 63 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑧𝑅𝑦 → ¬ 𝑧 ∈ 𝐷) → (𝑧 ∈ pred(𝑦, 𝐴, 𝑅) → ¬ 𝑧 ∈ 𝐷)) |
27 | 26 | alimi 1739 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑧(𝑧𝑅𝑦 → ¬ 𝑧 ∈ 𝐷) → ∀𝑧(𝑧 ∈ pred(𝑦, 𝐴, 𝑅) → ¬ 𝑧 ∈ 𝐷)) |
28 | 24, 27 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜃 → ∀𝑧(𝑧 ∈ pred(𝑦, 𝐴, 𝑅) → ¬ 𝑧 ∈ 𝐷)) |
29 | 28 | bnj1142 30860 |
. . . . . . . . . . . . 13
⊢ (𝜃 → ∀𝑧 ∈ pred (𝑦, 𝐴, 𝑅) ¬ 𝑧 ∈ 𝐷) |
30 | | bnj1523.8 |
. . . . . . . . . . . . . 14
⊢ 𝐷 = {𝑥 ∈ 𝐴 ∣ (𝐹‘𝑥) ≠ (𝐻‘𝑥)} |
31 | 5 | bnj1309 31090 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 ∈ 𝐵 → ∀𝑥 𝑤 ∈ 𝐵) |
32 | 7, 31 | bnj1307 31091 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 ∈ 𝐶 → ∀𝑥 𝑤 ∈ 𝐶) |
33 | 32 | nfcii 2755 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑥𝐶 |
34 | 33 | nfuni 4442 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑥∪ 𝐶 |
35 | 8, 34 | nfcxfr 2762 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑥𝐹 |
36 | 35 | nfcrii 2757 |
. . . . . . . . . . . . . 14
⊢ (𝑤 ∈ 𝐹 → ∀𝑥 𝑤 ∈ 𝐹) |
37 | 30, 36 | bnj1534 30923 |
. . . . . . . . . . . . 13
⊢ 𝐷 = {𝑧 ∈ 𝐴 ∣ (𝐹‘𝑧) ≠ (𝐻‘𝑧)} |
38 | 29, 18, 37 | bnj1533 30922 |
. . . . . . . . . . . 12
⊢ (𝜃 → ∀𝑧 ∈ pred (𝑦, 𝐴, 𝑅)(𝐹‘𝑧) = (𝐻‘𝑧)) |
39 | 13, 17, 19, 38 | bnj1536 30924 |
. . . . . . . . . . 11
⊢ (𝜃 → (𝐹 ↾ pred(𝑦, 𝐴, 𝑅)) = (𝐻 ↾ pred(𝑦, 𝐴, 𝑅))) |
40 | 39 | opeq2d 4409 |
. . . . . . . . . 10
⊢ (𝜃 → 〈𝑦, (𝐹 ↾ pred(𝑦, 𝐴, 𝑅))〉 = 〈𝑦, (𝐻 ↾ pred(𝑦, 𝐴, 𝑅))〉) |
41 | 40 | fveq2d 6195 |
. . . . . . . . 9
⊢ (𝜃 → (𝐺‘〈𝑦, (𝐹 ↾ pred(𝑦, 𝐴, 𝑅))〉) = (𝐺‘〈𝑦, (𝐻 ↾ pred(𝑦, 𝐴, 𝑅))〉)) |
42 | 5, 6, 7, 8 | bnj1500 31136 |
. . . . . . . . . . . . . . 15
⊢ (𝑅 FrSe 𝐴 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘〈𝑥, (𝐹 ↾ pred(𝑥, 𝐴, 𝑅))〉)) |
43 | 1, 42 | bnj835 30829 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘〈𝑥, (𝐹 ↾ pred(𝑥, 𝐴, 𝑅))〉)) |
44 | 2, 43 | bnj832 30828 |
. . . . . . . . . . . . 13
⊢ (𝜓 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘〈𝑥, (𝐹 ↾ pred(𝑥, 𝐴, 𝑅))〉)) |
45 | 4, 44 | bnj835 30829 |
. . . . . . . . . . . 12
⊢ (𝜒 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘〈𝑥, (𝐹 ↾ pred(𝑥, 𝐴, 𝑅))〉)) |
46 | 45, 36 | bnj1529 31138 |
. . . . . . . . . . 11
⊢ (𝜒 → ∀𝑦 ∈ 𝐴 (𝐹‘𝑦) = (𝐺‘〈𝑦, (𝐹 ↾ pred(𝑦, 𝐴, 𝑅))〉)) |
47 | 3, 46 | bnj835 30829 |
. . . . . . . . . 10
⊢ (𝜃 → ∀𝑦 ∈ 𝐴 (𝐹‘𝑦) = (𝐺‘〈𝑦, (𝐹 ↾ pred(𝑦, 𝐴, 𝑅))〉)) |
48 | 30 | ssrab3 3688 |
. . . . . . . . . . 11
⊢ 𝐷 ⊆ 𝐴 |
49 | 3 | simp2bi 1077 |
. . . . . . . . . . 11
⊢ (𝜃 → 𝑦 ∈ 𝐷) |
50 | 48, 49 | bnj1213 30869 |
. . . . . . . . . 10
⊢ (𝜃 → 𝑦 ∈ 𝐴) |
51 | 47, 50 | bnj1294 30888 |
. . . . . . . . 9
⊢ (𝜃 → (𝐹‘𝑦) = (𝐺‘〈𝑦, (𝐹 ↾ pred(𝑦, 𝐴, 𝑅))〉)) |
52 | 1 | simp3bi 1078 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝐻‘𝑥) = (𝐺‘〈𝑥, (𝐻 ↾ pred(𝑥, 𝐴, 𝑅))〉)) |
53 | 2, 52 | bnj832 30828 |
. . . . . . . . . . . . 13
⊢ (𝜓 → ∀𝑥 ∈ 𝐴 (𝐻‘𝑥) = (𝐺‘〈𝑥, (𝐻 ↾ pred(𝑥, 𝐴, 𝑅))〉)) |
54 | 4, 53 | bnj835 30829 |
. . . . . . . . . . . 12
⊢ (𝜒 → ∀𝑥 ∈ 𝐴 (𝐻‘𝑥) = (𝐺‘〈𝑥, (𝐻 ↾ pred(𝑥, 𝐴, 𝑅))〉)) |
55 | | ax-5 1839 |
. . . . . . . . . . . 12
⊢ (𝑣 ∈ 𝐻 → ∀𝑥 𝑣 ∈ 𝐻) |
56 | 54, 55 | bnj1529 31138 |
. . . . . . . . . . 11
⊢ (𝜒 → ∀𝑦 ∈ 𝐴 (𝐻‘𝑦) = (𝐺‘〈𝑦, (𝐻 ↾ pred(𝑦, 𝐴, 𝑅))〉)) |
57 | 3, 56 | bnj835 30829 |
. . . . . . . . . 10
⊢ (𝜃 → ∀𝑦 ∈ 𝐴 (𝐻‘𝑦) = (𝐺‘〈𝑦, (𝐻 ↾ pred(𝑦, 𝐴, 𝑅))〉)) |
58 | 57, 50 | bnj1294 30888 |
. . . . . . . . 9
⊢ (𝜃 → (𝐻‘𝑦) = (𝐺‘〈𝑦, (𝐻 ↾ pred(𝑦, 𝐴, 𝑅))〉)) |
59 | 41, 51, 58 | 3eqtr4d 2666 |
. . . . . . . 8
⊢ (𝜃 → (𝐹‘𝑦) = (𝐻‘𝑦)) |
60 | 30, 36 | bnj1534 30923 |
. . . . . . . . . . 11
⊢ 𝐷 = {𝑦 ∈ 𝐴 ∣ (𝐹‘𝑦) ≠ (𝐻‘𝑦)} |
61 | 60 | bnj1538 30925 |
. . . . . . . . . 10
⊢ (𝑦 ∈ 𝐷 → (𝐹‘𝑦) ≠ (𝐻‘𝑦)) |
62 | 3, 61 | bnj836 30830 |
. . . . . . . . 9
⊢ (𝜃 → (𝐹‘𝑦) ≠ (𝐻‘𝑦)) |
63 | 62 | neneqd 2799 |
. . . . . . . 8
⊢ (𝜃 → ¬ (𝐹‘𝑦) = (𝐻‘𝑦)) |
64 | 59, 63 | pm2.65i 185 |
. . . . . . 7
⊢ ¬
𝜃 |
65 | 64 | nex 1731 |
. . . . . 6
⊢ ¬
∃𝑦𝜃 |
66 | 1 | simp1bi 1076 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑅 FrSe 𝐴) |
67 | 2, 66 | bnj832 30828 |
. . . . . . . . 9
⊢ (𝜓 → 𝑅 FrSe 𝐴) |
68 | 4, 67 | bnj835 30829 |
. . . . . . . 8
⊢ (𝜒 → 𝑅 FrSe 𝐴) |
69 | 48 | a1i 11 |
. . . . . . . 8
⊢ (𝜒 → 𝐷 ⊆ 𝐴) |
70 | 4 | simp2bi 1077 |
. . . . . . . . . 10
⊢ (𝜒 → 𝑥 ∈ 𝐴) |
71 | 4 | simp3bi 1078 |
. . . . . . . . . 10
⊢ (𝜒 → (𝐹‘𝑥) ≠ (𝐻‘𝑥)) |
72 | 30 | rabeq2i 3197 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐷 ↔ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) ≠ (𝐻‘𝑥))) |
73 | 70, 71, 72 | sylanbrc 698 |
. . . . . . . . 9
⊢ (𝜒 → 𝑥 ∈ 𝐷) |
74 | | ne0i 3921 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐷 → 𝐷 ≠ ∅) |
75 | 73, 74 | syl 17 |
. . . . . . . 8
⊢ (𝜒 → 𝐷 ≠ ∅) |
76 | | bnj69 31078 |
. . . . . . . 8
⊢ ((𝑅 FrSe 𝐴 ∧ 𝐷 ⊆ 𝐴 ∧ 𝐷 ≠ ∅) → ∃𝑦 ∈ 𝐷 ∀𝑧 ∈ 𝐷 ¬ 𝑧𝑅𝑦) |
77 | 68, 69, 75, 76 | syl3anc 1326 |
. . . . . . 7
⊢ (𝜒 → ∃𝑦 ∈ 𝐷 ∀𝑧 ∈ 𝐷 ¬ 𝑧𝑅𝑦) |
78 | 77, 3 | bnj1209 30867 |
. . . . . 6
⊢ (𝜒 → ∃𝑦𝜃) |
79 | 65, 78 | mto 188 |
. . . . 5
⊢ ¬
𝜒 |
80 | 79 | nex 1731 |
. . . 4
⊢ ¬
∃𝑥𝜒 |
81 | 2 | simprbi 480 |
. . . . . 6
⊢ (𝜓 → 𝐹 ≠ 𝐻) |
82 | 11, 15, 81, 36 | bnj1542 30927 |
. . . . 5
⊢ (𝜓 → ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) ≠ (𝐻‘𝑥)) |
83 | 5, 6, 7, 8, 1, 2 | bnj1525 31137 |
. . . . 5
⊢ (𝜓 → ∀𝑥𝜓) |
84 | 82, 4, 83 | bnj1521 30921 |
. . . 4
⊢ (𝜓 → ∃𝑥𝜒) |
85 | 80, 84 | mto 188 |
. . 3
⊢ ¬
𝜓 |
86 | 2, 85 | bnj1541 30926 |
. 2
⊢ (𝜑 → 𝐹 = 𝐻) |
87 | 1, 86 | sylbir 225 |
1
⊢ ((𝑅 FrSe 𝐴 ∧ 𝐻 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐻‘𝑥) = (𝐺‘〈𝑥, (𝐻 ↾ pred(𝑥, 𝐴, 𝑅))〉)) → 𝐹 = 𝐻) |