Step | Hyp | Ref
| Expression |
1 | | cnvimass 5404 |
. . . . . . . . 9
⊢ (◡𝐹 “ {𝑢}) ⊆ dom 𝐹 |
2 | 1 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹) → (◡𝐹 “ {𝑢}) ⊆ dom 𝐹) |
3 | | wessf1ornlem.f |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹 Fn 𝐴) |
4 | | fndm 5904 |
. . . . . . . . . 10
⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴) |
5 | 3, 4 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → dom 𝐹 = 𝐴) |
6 | 5 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹) → dom 𝐹 = 𝐴) |
7 | 2, 6 | sseqtrd 3604 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹) → (◡𝐹 “ {𝑢}) ⊆ 𝐴) |
8 | | wessf1ornlem.r |
. . . . . . . . . 10
⊢ (𝜑 → 𝑅 We 𝐴) |
9 | 8 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹) → 𝑅 We 𝐴) |
10 | 1, 5 | syl5sseq 3616 |
. . . . . . . . . . 11
⊢ (𝜑 → (◡𝐹 “ {𝑢}) ⊆ 𝐴) |
11 | | wessf1ornlem.a |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
12 | | ssexg 4732 |
. . . . . . . . . . 11
⊢ (((◡𝐹 “ {𝑢}) ⊆ 𝐴 ∧ 𝐴 ∈ 𝑉) → (◡𝐹 “ {𝑢}) ∈ V) |
13 | 10, 11, 12 | syl2anc 691 |
. . . . . . . . . 10
⊢ (𝜑 → (◡𝐹 “ {𝑢}) ∈ V) |
14 | 13 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹) → (◡𝐹 “ {𝑢}) ∈ V) |
15 | | inisegn0 5416 |
. . . . . . . . . . 11
⊢ (𝑢 ∈ ran 𝐹 ↔ (◡𝐹 “ {𝑢}) ≠ ∅) |
16 | 15 | biimpi 205 |
. . . . . . . . . 10
⊢ (𝑢 ∈ ran 𝐹 → (◡𝐹 “ {𝑢}) ≠ ∅) |
17 | 16 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹) → (◡𝐹 “ {𝑢}) ≠ ∅) |
18 | | wereu 5034 |
. . . . . . . . 9
⊢ ((𝑅 We 𝐴 ∧ ((◡𝐹 “ {𝑢}) ∈ V ∧ (◡𝐹 “ {𝑢}) ⊆ 𝐴 ∧ (◡𝐹 “ {𝑢}) ≠ ∅)) → ∃!𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) |
19 | 9, 14, 7, 17, 18 | syl13anc 1320 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹) → ∃!𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) |
20 | | riotacl 6525 |
. . . . . . . 8
⊢
(∃!𝑣 ∈
(◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣 → (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) ∈ (◡𝐹 “ {𝑢})) |
21 | 19, 20 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹) → (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) ∈ (◡𝐹 “ {𝑢})) |
22 | 7, 21 | sseldd 3569 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹) → (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) ∈ 𝐴) |
23 | 22 | ralrimiva 2949 |
. . . . 5
⊢ (𝜑 → ∀𝑢 ∈ ran 𝐹(℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) ∈ 𝐴) |
24 | | wessf1ornlem.g |
. . . . . . 7
⊢ 𝐺 = (𝑦 ∈ ran 𝐹 ↦ (℩𝑥 ∈ (◡𝐹 “ {𝑦})∀𝑧 ∈ (◡𝐹 “ {𝑦}) ¬ 𝑧𝑅𝑥)) |
25 | | sneq 4135 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑢 → {𝑦} = {𝑢}) |
26 | 25 | imaeq2d 5385 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑢 → (◡𝐹 “ {𝑦}) = (◡𝐹 “ {𝑢})) |
27 | 26 | raleqdv 3121 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑢 → (∀𝑧 ∈ (◡𝐹 “ {𝑦}) ¬ 𝑧𝑅𝑥 ↔ ∀𝑧 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑧𝑅𝑥)) |
28 | 26, 27 | riotaeqbidv 6514 |
. . . . . . . . 9
⊢ (𝑦 = 𝑢 → (℩𝑥 ∈ (◡𝐹 “ {𝑦})∀𝑧 ∈ (◡𝐹 “ {𝑦}) ¬ 𝑧𝑅𝑥) = (℩𝑥 ∈ (◡𝐹 “ {𝑢})∀𝑧 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑧𝑅𝑥)) |
29 | | breq1 4586 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑡 → (𝑧𝑅𝑥 ↔ 𝑡𝑅𝑥)) |
30 | 29 | notbid 307 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑡 → (¬ 𝑧𝑅𝑥 ↔ ¬ 𝑡𝑅𝑥)) |
31 | 30 | cbvralv 3147 |
. . . . . . . . . . . . 13
⊢
(∀𝑧 ∈
(◡𝐹 “ {𝑢}) ¬ 𝑧𝑅𝑥 ↔ ∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑥) |
32 | 31 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑣 → (∀𝑧 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑧𝑅𝑥 ↔ ∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑥)) |
33 | | breq2 4587 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑣 → (𝑡𝑅𝑥 ↔ 𝑡𝑅𝑣)) |
34 | 33 | notbid 307 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑣 → (¬ 𝑡𝑅𝑥 ↔ ¬ 𝑡𝑅𝑣)) |
35 | 34 | ralbidv 2969 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑣 → (∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑥 ↔ ∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) |
36 | 32, 35 | bitrd 267 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑣 → (∀𝑧 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑧𝑅𝑥 ↔ ∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) |
37 | 36 | cbvriotav 6522 |
. . . . . . . . . 10
⊢
(℩𝑥
∈ (◡𝐹 “ {𝑢})∀𝑧 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑧𝑅𝑥) = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) |
38 | 37 | a1i 11 |
. . . . . . . . 9
⊢ (𝑦 = 𝑢 → (℩𝑥 ∈ (◡𝐹 “ {𝑢})∀𝑧 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑧𝑅𝑥) = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) |
39 | 28, 38 | eqtrd 2644 |
. . . . . . . 8
⊢ (𝑦 = 𝑢 → (℩𝑥 ∈ (◡𝐹 “ {𝑦})∀𝑧 ∈ (◡𝐹 “ {𝑦}) ¬ 𝑧𝑅𝑥) = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) |
40 | 39 | cbvmptv 4678 |
. . . . . . 7
⊢ (𝑦 ∈ ran 𝐹 ↦ (℩𝑥 ∈ (◡𝐹 “ {𝑦})∀𝑧 ∈ (◡𝐹 “ {𝑦}) ¬ 𝑧𝑅𝑥)) = (𝑢 ∈ ran 𝐹 ↦ (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) |
41 | 24, 40 | eqtri 2632 |
. . . . . 6
⊢ 𝐺 = (𝑢 ∈ ran 𝐹 ↦ (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) |
42 | 41 | rnmptss 6299 |
. . . . 5
⊢
(∀𝑢 ∈
ran 𝐹(℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) ∈ 𝐴 → ran 𝐺 ⊆ 𝐴) |
43 | 23, 42 | syl 17 |
. . . 4
⊢ (𝜑 → ran 𝐺 ⊆ 𝐴) |
44 | 11, 43 | ssexd 4733 |
. . . . 5
⊢ (𝜑 → ran 𝐺 ∈ V) |
45 | | elpwg 4116 |
. . . . 5
⊢ (ran
𝐺 ∈ V → (ran
𝐺 ∈ 𝒫 𝐴 ↔ ran 𝐺 ⊆ 𝐴)) |
46 | 44, 45 | syl 17 |
. . . 4
⊢ (𝜑 → (ran 𝐺 ∈ 𝒫 𝐴 ↔ ran 𝐺 ⊆ 𝐴)) |
47 | 43, 46 | mpbird 246 |
. . 3
⊢ (𝜑 → ran 𝐺 ∈ 𝒫 𝐴) |
48 | | dffn3 5967 |
. . . . . . . . . 10
⊢ (𝐹 Fn 𝐴 ↔ 𝐹:𝐴⟶ran 𝐹) |
49 | 48 | biimpi 205 |
. . . . . . . . 9
⊢ (𝐹 Fn 𝐴 → 𝐹:𝐴⟶ran 𝐹) |
50 | 3, 49 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐹:𝐴⟶ran 𝐹) |
51 | 50, 43 | fssresd 5984 |
. . . . . . 7
⊢ (𝜑 → (𝐹 ↾ ran 𝐺):ran 𝐺⟶ran 𝐹) |
52 | | simpl 472 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺)) → 𝜑) |
53 | | simprl 790 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺)) → 𝑤 ∈ ran 𝐺) |
54 | | simprr 792 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺)) → 𝑡 ∈ ran 𝐺) |
55 | | simpl 472 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ ((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑡)) → (𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺)) |
56 | | fvres 6117 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 ∈ ran 𝐺 → ((𝐹 ↾ ran 𝐺)‘𝑤) = (𝐹‘𝑤)) |
57 | 56 | eqcomd 2616 |
. . . . . . . . . . . . . 14
⊢ (𝑤 ∈ ran 𝐺 → (𝐹‘𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑤)) |
58 | 57 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ (((𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ ((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑡)) → (𝐹‘𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑤)) |
59 | | simpr 476 |
. . . . . . . . . . . . 13
⊢ (((𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ ((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑡)) → ((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑡)) |
60 | | fvres 6117 |
. . . . . . . . . . . . . 14
⊢ (𝑡 ∈ ran 𝐺 → ((𝐹 ↾ ran 𝐺)‘𝑡) = (𝐹‘𝑡)) |
61 | 60 | ad2antlr 759 |
. . . . . . . . . . . . 13
⊢ (((𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ ((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑡)) → ((𝐹 ↾ ran 𝐺)‘𝑡) = (𝐹‘𝑡)) |
62 | 58, 59, 61 | 3eqtrd 2648 |
. . . . . . . . . . . 12
⊢ (((𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ ((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑡)) → (𝐹‘𝑤) = (𝐹‘𝑡)) |
63 | 62 | 3adantl1 1210 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ ((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑡)) → (𝐹‘𝑤) = (𝐹‘𝑡)) |
64 | | simpl1 1057 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑤) = (𝐹‘𝑡)) → 𝜑) |
65 | | simpl3 1059 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑤) = (𝐹‘𝑡)) → 𝑡 ∈ ran 𝐺) |
66 | | vex 3176 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑤 ∈ V |
67 | 41 | elrnmpt 5293 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 ∈ V → (𝑤 ∈ ran 𝐺 ↔ ∃𝑢 ∈ ran 𝐹 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣))) |
68 | 66, 67 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 ∈ ran 𝐺 ↔ ∃𝑢 ∈ ran 𝐹 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) |
69 | 68 | biimpi 205 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 ∈ ran 𝐺 → ∃𝑢 ∈ ran 𝐹 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) |
70 | 69 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑤 ∈ ran 𝐺 ∧ (𝐹‘𝑤) = (𝐹‘𝑡)) → ∃𝑢 ∈ ran 𝐹 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) |
71 | 70 | 3ad2antl2 1217 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑤) = (𝐹‘𝑡)) → ∃𝑢 ∈ ran 𝐹 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) |
72 | 71, 68 | sylibr 223 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑤) = (𝐹‘𝑡)) → 𝑤 ∈ ran 𝐺) |
73 | | id 22 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹‘𝑤) = (𝐹‘𝑡) → (𝐹‘𝑤) = (𝐹‘𝑡)) |
74 | 73 | eqcomd 2616 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹‘𝑤) = (𝐹‘𝑡) → (𝐹‘𝑡) = (𝐹‘𝑤)) |
75 | 74 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑤) = (𝐹‘𝑡)) → (𝐹‘𝑡) = (𝐹‘𝑤)) |
76 | | eleq1 2676 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑏 = 𝑤 → (𝑏 ∈ ran 𝐺 ↔ 𝑤 ∈ ran 𝐺)) |
77 | 76 | 3anbi3d 1397 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 = 𝑤 → ((𝜑 ∧ 𝑡 ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺) ↔ (𝜑 ∧ 𝑡 ∈ ran 𝐺 ∧ 𝑤 ∈ ran 𝐺))) |
78 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑏 = 𝑤 → (𝐹‘𝑏) = (𝐹‘𝑤)) |
79 | 78 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 = 𝑤 → ((𝐹‘𝑡) = (𝐹‘𝑏) ↔ (𝐹‘𝑡) = (𝐹‘𝑤))) |
80 | 77, 79 | anbi12d 743 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 = 𝑤 → (((𝜑 ∧ 𝑡 ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺) ∧ (𝐹‘𝑡) = (𝐹‘𝑏)) ↔ ((𝜑 ∧ 𝑡 ∈ ran 𝐺 ∧ 𝑤 ∈ ran 𝐺) ∧ (𝐹‘𝑡) = (𝐹‘𝑤)))) |
81 | | breq1 4586 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 = 𝑤 → (𝑏𝑅𝑡 ↔ 𝑤𝑅𝑡)) |
82 | 81 | notbid 307 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 = 𝑤 → (¬ 𝑏𝑅𝑡 ↔ ¬ 𝑤𝑅𝑡)) |
83 | 80, 82 | imbi12d 333 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 = 𝑤 → ((((𝜑 ∧ 𝑡 ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺) ∧ (𝐹‘𝑡) = (𝐹‘𝑏)) → ¬ 𝑏𝑅𝑡) ↔ (((𝜑 ∧ 𝑡 ∈ ran 𝐺 ∧ 𝑤 ∈ ran 𝐺) ∧ (𝐹‘𝑡) = (𝐹‘𝑤)) → ¬ 𝑤𝑅𝑡))) |
84 | | eleq1 2676 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑎 = 𝑡 → (𝑎 ∈ ran 𝐺 ↔ 𝑡 ∈ ran 𝐺)) |
85 | 84 | 3anbi2d 1396 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 = 𝑡 → ((𝜑 ∧ 𝑎 ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺) ↔ (𝜑 ∧ 𝑡 ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺))) |
86 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑎 = 𝑡 → (𝐹‘𝑎) = (𝐹‘𝑡)) |
87 | 86 | eqeq1d 2612 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 = 𝑡 → ((𝐹‘𝑎) = (𝐹‘𝑏) ↔ (𝐹‘𝑡) = (𝐹‘𝑏))) |
88 | 85, 87 | anbi12d 743 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 = 𝑡 → (((𝜑 ∧ 𝑎 ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺) ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) ↔ ((𝜑 ∧ 𝑡 ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺) ∧ (𝐹‘𝑡) = (𝐹‘𝑏)))) |
89 | | breq2 4587 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 = 𝑡 → (𝑏𝑅𝑎 ↔ 𝑏𝑅𝑡)) |
90 | 89 | notbid 307 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 = 𝑡 → (¬ 𝑏𝑅𝑎 ↔ ¬ 𝑏𝑅𝑡)) |
91 | 88, 90 | imbi12d 333 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = 𝑡 → ((((𝜑 ∧ 𝑎 ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺) ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → ¬ 𝑏𝑅𝑎) ↔ (((𝜑 ∧ 𝑡 ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺) ∧ (𝐹‘𝑡) = (𝐹‘𝑏)) → ¬ 𝑏𝑅𝑡))) |
92 | | eleq1 2676 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑡 = 𝑏 → (𝑡 ∈ ran 𝐺 ↔ 𝑏 ∈ ran 𝐺)) |
93 | 92 | 3anbi3d 1397 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑡 = 𝑏 → ((𝜑 ∧ 𝑎 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ↔ (𝜑 ∧ 𝑎 ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺))) |
94 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑡 = 𝑏 → (𝐹‘𝑡) = (𝐹‘𝑏)) |
95 | 94 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑡 = 𝑏 → ((𝐹‘𝑎) = (𝐹‘𝑡) ↔ (𝐹‘𝑎) = (𝐹‘𝑏))) |
96 | 93, 95 | anbi12d 743 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑡 = 𝑏 → (((𝜑 ∧ 𝑎 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑎) = (𝐹‘𝑡)) ↔ ((𝜑 ∧ 𝑎 ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺) ∧ (𝐹‘𝑎) = (𝐹‘𝑏)))) |
97 | | breq1 4586 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑡 = 𝑏 → (𝑡𝑅𝑎 ↔ 𝑏𝑅𝑎)) |
98 | 97 | notbid 307 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑡 = 𝑏 → (¬ 𝑡𝑅𝑎 ↔ ¬ 𝑏𝑅𝑎)) |
99 | 96, 98 | imbi12d 333 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑡 = 𝑏 → ((((𝜑 ∧ 𝑎 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑎) = (𝐹‘𝑡)) → ¬ 𝑡𝑅𝑎) ↔ (((𝜑 ∧ 𝑎 ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺) ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → ¬ 𝑏𝑅𝑎))) |
100 | | eleq1 2676 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑤 = 𝑎 → (𝑤 ∈ ran 𝐺 ↔ 𝑎 ∈ ran 𝐺)) |
101 | 100 | 3anbi2d 1396 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑤 = 𝑎 → ((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ↔ (𝜑 ∧ 𝑎 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺))) |
102 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑤 = 𝑎 → (𝐹‘𝑤) = (𝐹‘𝑎)) |
103 | 102 | eqeq1d 2612 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑤 = 𝑎 → ((𝐹‘𝑤) = (𝐹‘𝑡) ↔ (𝐹‘𝑎) = (𝐹‘𝑡))) |
104 | 101, 103 | anbi12d 743 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 = 𝑎 → (((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑤) = (𝐹‘𝑡)) ↔ ((𝜑 ∧ 𝑎 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑎) = (𝐹‘𝑡)))) |
105 | | breq2 4587 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑤 = 𝑎 → (𝑡𝑅𝑤 ↔ 𝑡𝑅𝑎)) |
106 | 105 | notbid 307 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 = 𝑎 → (¬ 𝑡𝑅𝑤 ↔ ¬ 𝑡𝑅𝑎)) |
107 | 104, 106 | imbi12d 333 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 = 𝑎 → ((((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑤) = (𝐹‘𝑡)) → ¬ 𝑡𝑅𝑤) ↔ (((𝜑 ∧ 𝑎 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑎) = (𝐹‘𝑡)) → ¬ 𝑡𝑅𝑎))) |
108 | | nfv 1830 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
Ⅎ𝑢𝜑 |
109 | | nfcv 2751 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
Ⅎ𝑢𝑤 |
110 | | nfmpt1 4675 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
Ⅎ𝑢(𝑢 ∈ ran 𝐹 ↦ (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) |
111 | 41, 110 | nfcxfr 2749 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
Ⅎ𝑢𝐺 |
112 | 111 | nfrn 5289 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
Ⅎ𝑢ran
𝐺 |
113 | 109, 112 | nfel 2763 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
Ⅎ𝑢 𝑤 ∈ ran 𝐺 |
114 | 112 | nfcri 2745 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
Ⅎ𝑢 𝑡 ∈ ran 𝐺 |
115 | 108, 113,
114 | nf3an 1819 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑢(𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) |
116 | | nfv 1830 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑢(𝐹‘𝑤) = (𝐹‘𝑡) |
117 | 115, 116 | nfan 1816 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑢((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑤) = (𝐹‘𝑡)) |
118 | | nfv 1830 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑢 ¬ 𝑡𝑅𝑤 |
119 | | simp3 1056 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) |
120 | 119 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) = 𝑤) |
121 | | simp11 1084 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → 𝜑) |
122 | | simp2 1055 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → 𝑢 ∈ ran 𝐹) |
123 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) → 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) |
124 | | breq2 4587 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑣 = 𝑤 → (𝑡𝑅𝑣 ↔ 𝑡𝑅𝑤)) |
125 | 124 | notbid 307 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑣 = 𝑤 → (¬ 𝑡𝑅𝑣 ↔ ¬ 𝑡𝑅𝑤)) |
126 | 125 | ralbidv 2969 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑣 = 𝑤 → (∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣 ↔ ∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤)) |
127 | 126 | cbvriotav 6522 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(℩𝑣
∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) = (℩𝑤 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤) |
128 | 127 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) → (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) = (℩𝑤 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤)) |
129 | 123, 128 | eqtr2d 2645 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) → (℩𝑤 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤) = 𝑤) |
130 | 129 | 3ad2ant3 1077 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → (℩𝑤 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤) = 𝑤) |
131 | 126 | cbvreuv 3149 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(∃!𝑣 ∈
(◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣 ↔ ∃!𝑤 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤) |
132 | 19, 131 | sylib 207 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹) → ∃!𝑤 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤) |
133 | | riota1 6529 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(∃!𝑤 ∈
(◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤 → ((𝑤 ∈ (◡𝐹 “ {𝑢}) ∧ ∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤) ↔ (℩𝑤 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤) = 𝑤)) |
134 | 132, 133 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹) → ((𝑤 ∈ (◡𝐹 “ {𝑢}) ∧ ∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤) ↔ (℩𝑤 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤) = 𝑤)) |
135 | 134 | 3adant3 1074 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → ((𝑤 ∈ (◡𝐹 “ {𝑢}) ∧ ∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤) ↔ (℩𝑤 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤) = 𝑤)) |
136 | 130, 135 | mpbird 246 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → (𝑤 ∈ (◡𝐹 “ {𝑢}) ∧ ∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤)) |
137 | 136 | simpld 474 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → 𝑤 ∈ (◡𝐹 “ {𝑢})) |
138 | 121, 122,
119, 137 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → 𝑤 ∈ (◡𝐹 “ {𝑢})) |
139 | 121, 122,
19 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → ∃!𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) |
140 | 126 | riota2 6533 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑤 ∈ (◡𝐹 “ {𝑢}) ∧ ∃!𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) → (∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤 ↔ (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) = 𝑤)) |
141 | 138, 139,
140 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → (∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤 ↔ (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) = 𝑤)) |
142 | 120, 141 | mpbird 246 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → ∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤) |
143 | 142 | 3adant1r 1311 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑤) = (𝐹‘𝑡)) ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → ∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤) |
144 | 43 | sselda 3568 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑡 ∈ ran 𝐺) → 𝑡 ∈ 𝐴) |
145 | 144 | 3adant2 1073 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) → 𝑡 ∈ 𝐴) |
146 | 145 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑤) = (𝐹‘𝑡)) → 𝑡 ∈ 𝐴) |
147 | 146 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑤) = (𝐹‘𝑡)) ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → 𝑡 ∈ 𝐴) |
148 | 74 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑤) = (𝐹‘𝑡)) ∧ 𝑢 ∈ ran 𝐹) → (𝐹‘𝑡) = (𝐹‘𝑤)) |
149 | 148 | 3adant3 1074 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑤) = (𝐹‘𝑡)) ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → (𝐹‘𝑡) = (𝐹‘𝑤)) |
150 | | fniniseg 6246 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝐹 Fn 𝐴 → (𝑤 ∈ (◡𝐹 “ {𝑢}) ↔ (𝑤 ∈ 𝐴 ∧ (𝐹‘𝑤) = 𝑢))) |
151 | 121, 3, 150 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → (𝑤 ∈ (◡𝐹 “ {𝑢}) ↔ (𝑤 ∈ 𝐴 ∧ (𝐹‘𝑤) = 𝑢))) |
152 | 138, 151 | mpbid 221 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → (𝑤 ∈ 𝐴 ∧ (𝐹‘𝑤) = 𝑢)) |
153 | 152 | simprd 478 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → (𝐹‘𝑤) = 𝑢) |
154 | 153 | 3adant1r 1311 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑤) = (𝐹‘𝑡)) ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → (𝐹‘𝑤) = 𝑢) |
155 | 149, 154 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑤) = (𝐹‘𝑡)) ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → (𝐹‘𝑡) = 𝑢) |
156 | 147, 155 | jca 553 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑤) = (𝐹‘𝑡)) ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → (𝑡 ∈ 𝐴 ∧ (𝐹‘𝑡) = 𝑢)) |
157 | | fniniseg 6246 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝐹 Fn 𝐴 → (𝑡 ∈ (◡𝐹 “ {𝑢}) ↔ (𝑡 ∈ 𝐴 ∧ (𝐹‘𝑡) = 𝑢))) |
158 | 3, 157 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → (𝑡 ∈ (◡𝐹 “ {𝑢}) ↔ (𝑡 ∈ 𝐴 ∧ (𝐹‘𝑡) = 𝑢))) |
159 | 158 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) → (𝑡 ∈ (◡𝐹 “ {𝑢}) ↔ (𝑡 ∈ 𝐴 ∧ (𝐹‘𝑡) = 𝑢))) |
160 | 159 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑤) = (𝐹‘𝑡)) ∧ 𝑢 ∈ ran 𝐹) → (𝑡 ∈ (◡𝐹 “ {𝑢}) ↔ (𝑡 ∈ 𝐴 ∧ (𝐹‘𝑡) = 𝑢))) |
161 | 160 | 3adant3 1074 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑤) = (𝐹‘𝑡)) ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → (𝑡 ∈ (◡𝐹 “ {𝑢}) ↔ (𝑡 ∈ 𝐴 ∧ (𝐹‘𝑡) = 𝑢))) |
162 | 156, 161 | mpbird 246 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑤) = (𝐹‘𝑡)) ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → 𝑡 ∈ (◡𝐹 “ {𝑢})) |
163 | | rspa 2914 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((∀𝑡 ∈
(◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑤 ∧ 𝑡 ∈ (◡𝐹 “ {𝑢})) → ¬ 𝑡𝑅𝑤) |
164 | 143, 162,
163 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑤) = (𝐹‘𝑡)) ∧ 𝑢 ∈ ran 𝐹 ∧ 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) → ¬ 𝑡𝑅𝑤) |
165 | 164 | 3exp 1256 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑤) = (𝐹‘𝑡)) → (𝑢 ∈ ran 𝐹 → (𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) → ¬ 𝑡𝑅𝑤))) |
166 | 117, 118,
165 | rexlimd 3008 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑤) = (𝐹‘𝑡)) → (∃𝑢 ∈ ran 𝐹 𝑤 = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) → ¬ 𝑡𝑅𝑤)) |
167 | 71, 166 | mpd 15 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑤) = (𝐹‘𝑡)) → ¬ 𝑡𝑅𝑤) |
168 | 107, 167 | chvarv 2251 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑎 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑎) = (𝐹‘𝑡)) → ¬ 𝑡𝑅𝑎) |
169 | 99, 168 | chvarv 2251 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑎 ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺) ∧ (𝐹‘𝑎) = (𝐹‘𝑏)) → ¬ 𝑏𝑅𝑎) |
170 | 91, 169 | chvarv 2251 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑡 ∈ ran 𝐺 ∧ 𝑏 ∈ ran 𝐺) ∧ (𝐹‘𝑡) = (𝐹‘𝑏)) → ¬ 𝑏𝑅𝑡) |
171 | 83, 170 | chvarv 2251 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑡 ∈ ran 𝐺 ∧ 𝑤 ∈ ran 𝐺) ∧ (𝐹‘𝑡) = (𝐹‘𝑤)) → ¬ 𝑤𝑅𝑡) |
172 | 64, 65, 72, 75, 171 | syl31anc 1321 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑤) = (𝐹‘𝑡)) → ¬ 𝑤𝑅𝑡) |
173 | 172, 167 | jca 553 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑤) = (𝐹‘𝑡)) → (¬ 𝑤𝑅𝑡 ∧ ¬ 𝑡𝑅𝑤)) |
174 | | weso 5029 |
. . . . . . . . . . . . . . . 16
⊢ (𝑅 We 𝐴 → 𝑅 Or 𝐴) |
175 | 8, 174 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑅 Or 𝐴) |
176 | 175 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝐹‘𝑤) = (𝐹‘𝑡)) → 𝑅 Or 𝐴) |
177 | 176 | 3ad2antl1 1216 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑤) = (𝐹‘𝑡)) → 𝑅 Or 𝐴) |
178 | 43 | sselda 3568 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑤 ∈ ran 𝐺) → 𝑤 ∈ 𝐴) |
179 | 178 | 3adant3 1074 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) → 𝑤 ∈ 𝐴) |
180 | 179 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑤) = (𝐹‘𝑡)) → 𝑤 ∈ 𝐴) |
181 | | sotrieq2 4987 |
. . . . . . . . . . . . 13
⊢ ((𝑅 Or 𝐴 ∧ (𝑤 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴)) → (𝑤 = 𝑡 ↔ (¬ 𝑤𝑅𝑡 ∧ ¬ 𝑡𝑅𝑤))) |
182 | 177, 180,
146, 181 | syl12anc 1316 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑤) = (𝐹‘𝑡)) → (𝑤 = 𝑡 ↔ (¬ 𝑤𝑅𝑡 ∧ ¬ 𝑡𝑅𝑤))) |
183 | 173, 182 | mpbird 246 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ (𝐹‘𝑤) = (𝐹‘𝑡)) → 𝑤 = 𝑡) |
184 | 55, 63, 183 | syl2anc 691 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) ∧ ((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑡)) → 𝑤 = 𝑡) |
185 | 184 | ex 449 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺) → (((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑡) → 𝑤 = 𝑡)) |
186 | 52, 53, 54, 185 | syl3anc 1318 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑤 ∈ ran 𝐺 ∧ 𝑡 ∈ ran 𝐺)) → (((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑡) → 𝑤 = 𝑡)) |
187 | 186 | ralrimivva 2954 |
. . . . . . 7
⊢ (𝜑 → ∀𝑤 ∈ ran 𝐺∀𝑡 ∈ ran 𝐺(((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑡) → 𝑤 = 𝑡)) |
188 | 51, 187 | jca 553 |
. . . . . 6
⊢ (𝜑 → ((𝐹 ↾ ran 𝐺):ran 𝐺⟶ran 𝐹 ∧ ∀𝑤 ∈ ran 𝐺∀𝑡 ∈ ran 𝐺(((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑡) → 𝑤 = 𝑡))) |
189 | | dff13 6416 |
. . . . . 6
⊢ ((𝐹 ↾ ran 𝐺):ran 𝐺–1-1→ran 𝐹 ↔ ((𝐹 ↾ ran 𝐺):ran 𝐺⟶ran 𝐹 ∧ ∀𝑤 ∈ ran 𝐺∀𝑡 ∈ ran 𝐺(((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘𝑡) → 𝑤 = 𝑡))) |
190 | 188, 189 | sylibr 223 |
. . . . 5
⊢ (𝜑 → (𝐹 ↾ ran 𝐺):ran 𝐺–1-1→ran 𝐹) |
191 | | riotaex 6515 |
. . . . . . . . . . . . . 14
⊢
(℩𝑣
∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) ∈ V |
192 | 191 | rgenw 2908 |
. . . . . . . . . . . . 13
⊢
∀𝑢 ∈ ran
𝐹(℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) ∈ V |
193 | 192 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑢 ∈ ran 𝐹(℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) ∈ V) |
194 | 41 | fnmpt 5933 |
. . . . . . . . . . . 12
⊢
(∀𝑢 ∈
ran 𝐹(℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) ∈ V → 𝐺 Fn ran 𝐹) |
195 | 193, 194 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐺 Fn ran 𝐹) |
196 | | dffn3 5967 |
. . . . . . . . . . . 12
⊢ (𝐺 Fn ran 𝐹 ↔ 𝐺:ran 𝐹⟶ran 𝐺) |
197 | 196 | biimpi 205 |
. . . . . . . . . . 11
⊢ (𝐺 Fn ran 𝐹 → 𝐺:ran 𝐹⟶ran 𝐺) |
198 | 195, 197 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐺:ran 𝐹⟶ran 𝐺) |
199 | 198 | ffvelrnda 6267 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹) → (𝐺‘𝑢) ∈ ran 𝐺) |
200 | | fvres 6117 |
. . . . . . . . . . 11
⊢ ((𝐺‘𝑢) ∈ ran 𝐺 → ((𝐹 ↾ ran 𝐺)‘(𝐺‘𝑢)) = (𝐹‘(𝐺‘𝑢))) |
201 | 199, 200 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹) → ((𝐹 ↾ ran 𝐺)‘(𝐺‘𝑢)) = (𝐹‘(𝐺‘𝑢))) |
202 | 17, 15 | sylibr 223 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹) → 𝑢 ∈ ran 𝐹) |
203 | 191 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹) → (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) ∈ V) |
204 | 41 | fvmpt2 6200 |
. . . . . . . . . . . . . 14
⊢ ((𝑢 ∈ ran 𝐹 ∧ (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) ∈ V) → (𝐺‘𝑢) = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) |
205 | 202, 203,
204 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹) → (𝐺‘𝑢) = (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) |
206 | 205, 21 | eqeltrd 2688 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹) → (𝐺‘𝑢) ∈ (◡𝐹 “ {𝑢})) |
207 | | fvex 6113 |
. . . . . . . . . . . . . 14
⊢ (𝐺‘𝑢) ∈ V |
208 | | eleq1 2676 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 = (𝐺‘𝑢) → (𝑤 ∈ (◡𝐹 “ {𝑢}) ↔ (𝐺‘𝑢) ∈ (◡𝐹 “ {𝑢}))) |
209 | | eleq1 2676 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 = (𝐺‘𝑢) → (𝑤 ∈ 𝐴 ↔ (𝐺‘𝑢) ∈ 𝐴)) |
210 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 = (𝐺‘𝑢) → (𝐹‘𝑤) = (𝐹‘(𝐺‘𝑢))) |
211 | 210 | eqeq1d 2612 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 = (𝐺‘𝑢) → ((𝐹‘𝑤) = 𝑢 ↔ (𝐹‘(𝐺‘𝑢)) = 𝑢)) |
212 | 209, 211 | anbi12d 743 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 = (𝐺‘𝑢) → ((𝑤 ∈ 𝐴 ∧ (𝐹‘𝑤) = 𝑢) ↔ ((𝐺‘𝑢) ∈ 𝐴 ∧ (𝐹‘(𝐺‘𝑢)) = 𝑢))) |
213 | 208, 212 | bibi12d 334 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = (𝐺‘𝑢) → ((𝑤 ∈ (◡𝐹 “ {𝑢}) ↔ (𝑤 ∈ 𝐴 ∧ (𝐹‘𝑤) = 𝑢)) ↔ ((𝐺‘𝑢) ∈ (◡𝐹 “ {𝑢}) ↔ ((𝐺‘𝑢) ∈ 𝐴 ∧ (𝐹‘(𝐺‘𝑢)) = 𝑢)))) |
214 | 213 | imbi2d 329 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = (𝐺‘𝑢) → ((𝜑 → (𝑤 ∈ (◡𝐹 “ {𝑢}) ↔ (𝑤 ∈ 𝐴 ∧ (𝐹‘𝑤) = 𝑢))) ↔ (𝜑 → ((𝐺‘𝑢) ∈ (◡𝐹 “ {𝑢}) ↔ ((𝐺‘𝑢) ∈ 𝐴 ∧ (𝐹‘(𝐺‘𝑢)) = 𝑢))))) |
215 | 3, 150 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑤 ∈ (◡𝐹 “ {𝑢}) ↔ (𝑤 ∈ 𝐴 ∧ (𝐹‘𝑤) = 𝑢))) |
216 | 207, 214,
215 | vtocl 3232 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐺‘𝑢) ∈ (◡𝐹 “ {𝑢}) ↔ ((𝐺‘𝑢) ∈ 𝐴 ∧ (𝐹‘(𝐺‘𝑢)) = 𝑢))) |
217 | 216 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹) → ((𝐺‘𝑢) ∈ (◡𝐹 “ {𝑢}) ↔ ((𝐺‘𝑢) ∈ 𝐴 ∧ (𝐹‘(𝐺‘𝑢)) = 𝑢))) |
218 | 206, 217 | mpbid 221 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹) → ((𝐺‘𝑢) ∈ 𝐴 ∧ (𝐹‘(𝐺‘𝑢)) = 𝑢)) |
219 | 218 | simprd 478 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹) → (𝐹‘(𝐺‘𝑢)) = 𝑢) |
220 | 201, 219 | eqtr2d 2645 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹) → 𝑢 = ((𝐹 ↾ ran 𝐺)‘(𝐺‘𝑢))) |
221 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑤 = (𝐺‘𝑢) → ((𝐹 ↾ ran 𝐺)‘𝑤) = ((𝐹 ↾ ran 𝐺)‘(𝐺‘𝑢))) |
222 | 221 | eqeq2d 2620 |
. . . . . . . . . 10
⊢ (𝑤 = (𝐺‘𝑢) → (𝑢 = ((𝐹 ↾ ran 𝐺)‘𝑤) ↔ 𝑢 = ((𝐹 ↾ ran 𝐺)‘(𝐺‘𝑢)))) |
223 | 222 | rspcev 3282 |
. . . . . . . . 9
⊢ (((𝐺‘𝑢) ∈ ran 𝐺 ∧ 𝑢 = ((𝐹 ↾ ran 𝐺)‘(𝐺‘𝑢))) → ∃𝑤 ∈ ran 𝐺 𝑢 = ((𝐹 ↾ ran 𝐺)‘𝑤)) |
224 | 199, 220,
223 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑢 ∈ ran 𝐹) → ∃𝑤 ∈ ran 𝐺 𝑢 = ((𝐹 ↾ ran 𝐺)‘𝑤)) |
225 | 224 | ralrimiva 2949 |
. . . . . . 7
⊢ (𝜑 → ∀𝑢 ∈ ran 𝐹∃𝑤 ∈ ran 𝐺 𝑢 = ((𝐹 ↾ ran 𝐺)‘𝑤)) |
226 | 51, 225 | jca 553 |
. . . . . 6
⊢ (𝜑 → ((𝐹 ↾ ran 𝐺):ran 𝐺⟶ran 𝐹 ∧ ∀𝑢 ∈ ran 𝐹∃𝑤 ∈ ran 𝐺 𝑢 = ((𝐹 ↾ ran 𝐺)‘𝑤))) |
227 | | dffo3 6282 |
. . . . . 6
⊢ ((𝐹 ↾ ran 𝐺):ran 𝐺–onto→ran 𝐹 ↔ ((𝐹 ↾ ran 𝐺):ran 𝐺⟶ran 𝐹 ∧ ∀𝑢 ∈ ran 𝐹∃𝑤 ∈ ran 𝐺 𝑢 = ((𝐹 ↾ ran 𝐺)‘𝑤))) |
228 | 226, 227 | sylibr 223 |
. . . . 5
⊢ (𝜑 → (𝐹 ↾ ran 𝐺):ran 𝐺–onto→ran 𝐹) |
229 | 190, 228 | jca 553 |
. . . 4
⊢ (𝜑 → ((𝐹 ↾ ran 𝐺):ran 𝐺–1-1→ran 𝐹 ∧ (𝐹 ↾ ran 𝐺):ran 𝐺–onto→ran 𝐹)) |
230 | | df-f1o 5811 |
. . . 4
⊢ ((𝐹 ↾ ran 𝐺):ran 𝐺–1-1-onto→ran
𝐹 ↔ ((𝐹 ↾ ran 𝐺):ran 𝐺–1-1→ran 𝐹 ∧ (𝐹 ↾ ran 𝐺):ran 𝐺–onto→ran 𝐹)) |
231 | 229, 230 | sylibr 223 |
. . 3
⊢ (𝜑 → (𝐹 ↾ ran 𝐺):ran 𝐺–1-1-onto→ran
𝐹) |
232 | | nfcv 2751 |
. . . . . 6
⊢
Ⅎ𝑣𝐹 |
233 | | nfcv 2751 |
. . . . . . . . 9
⊢
Ⅎ𝑣ran
𝐹 |
234 | | nfriota1 6518 |
. . . . . . . . 9
⊢
Ⅎ𝑣(℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣) |
235 | 233, 234 | nfmpt 4674 |
. . . . . . . 8
⊢
Ⅎ𝑣(𝑢 ∈ ran 𝐹 ↦ (℩𝑣 ∈ (◡𝐹 “ {𝑢})∀𝑡 ∈ (◡𝐹 “ {𝑢}) ¬ 𝑡𝑅𝑣)) |
236 | 41, 235 | nfcxfr 2749 |
. . . . . . 7
⊢
Ⅎ𝑣𝐺 |
237 | 236 | nfrn 5289 |
. . . . . 6
⊢
Ⅎ𝑣ran
𝐺 |
238 | 232, 237 | nfres 5319 |
. . . . 5
⊢
Ⅎ𝑣(𝐹 ↾ ran 𝐺) |
239 | 238, 237,
233 | nff1o 6048 |
. . . 4
⊢
Ⅎ𝑣(𝐹 ↾ ran 𝐺):ran 𝐺–1-1-onto→ran
𝐹 |
240 | | reseq2 5312 |
. . . . 5
⊢ (𝑣 = ran 𝐺 → (𝐹 ↾ 𝑣) = (𝐹 ↾ ran 𝐺)) |
241 | | id 22 |
. . . . 5
⊢ (𝑣 = ran 𝐺 → 𝑣 = ran 𝐺) |
242 | | eqidd 2611 |
. . . . 5
⊢ (𝑣 = ran 𝐺 → ran 𝐹 = ran 𝐹) |
243 | 240, 241,
242 | f1oeq123d 6046 |
. . . 4
⊢ (𝑣 = ran 𝐺 → ((𝐹 ↾ 𝑣):𝑣–1-1-onto→ran
𝐹 ↔ (𝐹 ↾ ran 𝐺):ran 𝐺–1-1-onto→ran
𝐹)) |
244 | 239, 243 | rspce 3277 |
. . 3
⊢ ((ran
𝐺 ∈ 𝒫 𝐴 ∧ (𝐹 ↾ ran 𝐺):ran 𝐺–1-1-onto→ran
𝐹) → ∃𝑣 ∈ 𝒫 𝐴(𝐹 ↾ 𝑣):𝑣–1-1-onto→ran
𝐹) |
245 | 47, 231, 244 | syl2anc 691 |
. 2
⊢ (𝜑 → ∃𝑣 ∈ 𝒫 𝐴(𝐹 ↾ 𝑣):𝑣–1-1-onto→ran
𝐹) |
246 | | reseq2 5312 |
. . . 4
⊢ (𝑣 = 𝑥 → (𝐹 ↾ 𝑣) = (𝐹 ↾ 𝑥)) |
247 | | id 22 |
. . . 4
⊢ (𝑣 = 𝑥 → 𝑣 = 𝑥) |
248 | | eqidd 2611 |
. . . 4
⊢ (𝑣 = 𝑥 → ran 𝐹 = ran 𝐹) |
249 | 246, 247,
248 | f1oeq123d 6046 |
. . 3
⊢ (𝑣 = 𝑥 → ((𝐹 ↾ 𝑣):𝑣–1-1-onto→ran
𝐹 ↔ (𝐹 ↾ 𝑥):𝑥–1-1-onto→ran
𝐹)) |
250 | 249 | cbvrexv 3148 |
. 2
⊢
(∃𝑣 ∈
𝒫 𝐴(𝐹 ↾ 𝑣):𝑣–1-1-onto→ran
𝐹 ↔ ∃𝑥 ∈ 𝒫 𝐴(𝐹 ↾ 𝑥):𝑥–1-1-onto→ran
𝐹) |
251 | 245, 250 | sylib 207 |
1
⊢ (𝜑 → ∃𝑥 ∈ 𝒫 𝐴(𝐹 ↾ 𝑥):𝑥–1-1-onto→ran
𝐹) |