Step |
Hyp |
Ref |
Expression |
1 |
|
fphpd.a |
⊢ ( 𝜑 → 𝐵 ≺ 𝐴 ) |
2 |
|
fphpd.b |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝐵 ) |
3 |
|
fphpd.c |
⊢ ( 𝑥 = 𝑦 → 𝐶 = 𝐷 ) |
4 |
|
domnsym |
⊢ ( 𝐴 ≼ 𝐵 → ¬ 𝐵 ≺ 𝐴 ) |
5 |
4 1
|
nsyl3 |
⊢ ( 𝜑 → ¬ 𝐴 ≼ 𝐵 ) |
6 |
|
relsdom |
⊢ Rel ≺ |
7 |
6
|
brrelex1i |
⊢ ( 𝐵 ≺ 𝐴 → 𝐵 ∈ V ) |
8 |
1 7
|
syl |
⊢ ( 𝜑 → 𝐵 ∈ V ) |
9 |
8
|
adantr |
⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝐶 = 𝐷 → 𝑥 = 𝑦 ) ) → 𝐵 ∈ V ) |
10 |
|
nfv |
⊢ Ⅎ 𝑥 ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) |
11 |
|
nfcsb1v |
⊢ Ⅎ 𝑥 ⦋ 𝑎 / 𝑥 ⦌ 𝐶 |
12 |
11
|
nfel1 |
⊢ Ⅎ 𝑥 ⦋ 𝑎 / 𝑥 ⦌ 𝐶 ∈ 𝐵 |
13 |
10 12
|
nfim |
⊢ Ⅎ 𝑥 ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ⦋ 𝑎 / 𝑥 ⦌ 𝐶 ∈ 𝐵 ) |
14 |
|
eleq1w |
⊢ ( 𝑥 = 𝑎 → ( 𝑥 ∈ 𝐴 ↔ 𝑎 ∈ 𝐴 ) ) |
15 |
14
|
anbi2d |
⊢ ( 𝑥 = 𝑎 → ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ↔ ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ) ) |
16 |
|
csbeq1a |
⊢ ( 𝑥 = 𝑎 → 𝐶 = ⦋ 𝑎 / 𝑥 ⦌ 𝐶 ) |
17 |
16
|
eleq1d |
⊢ ( 𝑥 = 𝑎 → ( 𝐶 ∈ 𝐵 ↔ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 ∈ 𝐵 ) ) |
18 |
15 17
|
imbi12d |
⊢ ( 𝑥 = 𝑎 → ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝐵 ) ↔ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ⦋ 𝑎 / 𝑥 ⦌ 𝐶 ∈ 𝐵 ) ) ) |
19 |
13 18 2
|
chvarfv |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ⦋ 𝑎 / 𝑥 ⦌ 𝐶 ∈ 𝐵 ) |
20 |
19
|
ex |
⊢ ( 𝜑 → ( 𝑎 ∈ 𝐴 → ⦋ 𝑎 / 𝑥 ⦌ 𝐶 ∈ 𝐵 ) ) |
21 |
20
|
adantr |
⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝐶 = 𝐷 → 𝑥 = 𝑦 ) ) → ( 𝑎 ∈ 𝐴 → ⦋ 𝑎 / 𝑥 ⦌ 𝐶 ∈ 𝐵 ) ) |
22 |
|
csbid |
⊢ ⦋ 𝑥 / 𝑥 ⦌ 𝐶 = 𝐶 |
23 |
|
vex |
⊢ 𝑦 ∈ V |
24 |
23 3
|
csbie |
⊢ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 = 𝐷 |
25 |
22 24
|
eqeq12i |
⊢ ( ⦋ 𝑥 / 𝑥 ⦌ 𝐶 = ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ↔ 𝐶 = 𝐷 ) |
26 |
25
|
imbi1i |
⊢ ( ( ⦋ 𝑥 / 𝑥 ⦌ 𝐶 = ⦋ 𝑦 / 𝑥 ⦌ 𝐶 → 𝑥 = 𝑦 ) ↔ ( 𝐶 = 𝐷 → 𝑥 = 𝑦 ) ) |
27 |
26
|
2ralbii |
⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ⦋ 𝑥 / 𝑥 ⦌ 𝐶 = ⦋ 𝑦 / 𝑥 ⦌ 𝐶 → 𝑥 = 𝑦 ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝐶 = 𝐷 → 𝑥 = 𝑦 ) ) |
28 |
|
nfcsb1v |
⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐶 |
29 |
11 28
|
nfeq |
⊢ Ⅎ 𝑥 ⦋ 𝑎 / 𝑥 ⦌ 𝐶 = ⦋ 𝑦 / 𝑥 ⦌ 𝐶 |
30 |
|
nfv |
⊢ Ⅎ 𝑥 𝑎 = 𝑦 |
31 |
29 30
|
nfim |
⊢ Ⅎ 𝑥 ( ⦋ 𝑎 / 𝑥 ⦌ 𝐶 = ⦋ 𝑦 / 𝑥 ⦌ 𝐶 → 𝑎 = 𝑦 ) |
32 |
|
nfv |
⊢ Ⅎ 𝑦 ( ⦋ 𝑎 / 𝑥 ⦌ 𝐶 = ⦋ 𝑏 / 𝑥 ⦌ 𝐶 → 𝑎 = 𝑏 ) |
33 |
|
csbeq1 |
⊢ ( 𝑥 = 𝑎 → ⦋ 𝑥 / 𝑥 ⦌ 𝐶 = ⦋ 𝑎 / 𝑥 ⦌ 𝐶 ) |
34 |
33
|
eqeq1d |
⊢ ( 𝑥 = 𝑎 → ( ⦋ 𝑥 / 𝑥 ⦌ 𝐶 = ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ↔ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 = ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) ) |
35 |
|
equequ1 |
⊢ ( 𝑥 = 𝑎 → ( 𝑥 = 𝑦 ↔ 𝑎 = 𝑦 ) ) |
36 |
34 35
|
imbi12d |
⊢ ( 𝑥 = 𝑎 → ( ( ⦋ 𝑥 / 𝑥 ⦌ 𝐶 = ⦋ 𝑦 / 𝑥 ⦌ 𝐶 → 𝑥 = 𝑦 ) ↔ ( ⦋ 𝑎 / 𝑥 ⦌ 𝐶 = ⦋ 𝑦 / 𝑥 ⦌ 𝐶 → 𝑎 = 𝑦 ) ) ) |
37 |
|
csbeq1 |
⊢ ( 𝑦 = 𝑏 → ⦋ 𝑦 / 𝑥 ⦌ 𝐶 = ⦋ 𝑏 / 𝑥 ⦌ 𝐶 ) |
38 |
37
|
eqeq2d |
⊢ ( 𝑦 = 𝑏 → ( ⦋ 𝑎 / 𝑥 ⦌ 𝐶 = ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ↔ ⦋ 𝑎 / 𝑥 ⦌ 𝐶 = ⦋ 𝑏 / 𝑥 ⦌ 𝐶 ) ) |
39 |
|
equequ2 |
⊢ ( 𝑦 = 𝑏 → ( 𝑎 = 𝑦 ↔ 𝑎 = 𝑏 ) ) |
40 |
38 39
|
imbi12d |
⊢ ( 𝑦 = 𝑏 → ( ( ⦋ 𝑎 / 𝑥 ⦌ 𝐶 = ⦋ 𝑦 / 𝑥 ⦌ 𝐶 → 𝑎 = 𝑦 ) ↔ ( ⦋ 𝑎 / 𝑥 ⦌ 𝐶 = ⦋ 𝑏 / 𝑥 ⦌ 𝐶 → 𝑎 = 𝑏 ) ) ) |
41 |
31 32 36 40
|
rspc2 |
⊢ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ⦋ 𝑥 / 𝑥 ⦌ 𝐶 = ⦋ 𝑦 / 𝑥 ⦌ 𝐶 → 𝑥 = 𝑦 ) → ( ⦋ 𝑎 / 𝑥 ⦌ 𝐶 = ⦋ 𝑏 / 𝑥 ⦌ 𝐶 → 𝑎 = 𝑏 ) ) ) |
42 |
41
|
com12 |
⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ⦋ 𝑥 / 𝑥 ⦌ 𝐶 = ⦋ 𝑦 / 𝑥 ⦌ 𝐶 → 𝑥 = 𝑦 ) → ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) → ( ⦋ 𝑎 / 𝑥 ⦌ 𝐶 = ⦋ 𝑏 / 𝑥 ⦌ 𝐶 → 𝑎 = 𝑏 ) ) ) |
43 |
27 42
|
sylbir |
⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝐶 = 𝐷 → 𝑥 = 𝑦 ) → ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) → ( ⦋ 𝑎 / 𝑥 ⦌ 𝐶 = ⦋ 𝑏 / 𝑥 ⦌ 𝐶 → 𝑎 = 𝑏 ) ) ) |
44 |
|
id |
⊢ ( ( ⦋ 𝑎 / 𝑥 ⦌ 𝐶 = ⦋ 𝑏 / 𝑥 ⦌ 𝐶 → 𝑎 = 𝑏 ) → ( ⦋ 𝑎 / 𝑥 ⦌ 𝐶 = ⦋ 𝑏 / 𝑥 ⦌ 𝐶 → 𝑎 = 𝑏 ) ) |
45 |
|
csbeq1 |
⊢ ( 𝑎 = 𝑏 → ⦋ 𝑎 / 𝑥 ⦌ 𝐶 = ⦋ 𝑏 / 𝑥 ⦌ 𝐶 ) |
46 |
44 45
|
impbid1 |
⊢ ( ( ⦋ 𝑎 / 𝑥 ⦌ 𝐶 = ⦋ 𝑏 / 𝑥 ⦌ 𝐶 → 𝑎 = 𝑏 ) → ( ⦋ 𝑎 / 𝑥 ⦌ 𝐶 = ⦋ 𝑏 / 𝑥 ⦌ 𝐶 ↔ 𝑎 = 𝑏 ) ) |
47 |
43 46
|
syl6 |
⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝐶 = 𝐷 → 𝑥 = 𝑦 ) → ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) → ( ⦋ 𝑎 / 𝑥 ⦌ 𝐶 = ⦋ 𝑏 / 𝑥 ⦌ 𝐶 ↔ 𝑎 = 𝑏 ) ) ) |
48 |
47
|
adantl |
⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝐶 = 𝐷 → 𝑥 = 𝑦 ) ) → ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴 ) → ( ⦋ 𝑎 / 𝑥 ⦌ 𝐶 = ⦋ 𝑏 / 𝑥 ⦌ 𝐶 ↔ 𝑎 = 𝑏 ) ) ) |
49 |
21 48
|
dom2d |
⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝐶 = 𝐷 → 𝑥 = 𝑦 ) ) → ( 𝐵 ∈ V → 𝐴 ≼ 𝐵 ) ) |
50 |
9 49
|
mpd |
⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝐶 = 𝐷 → 𝑥 = 𝑦 ) ) → 𝐴 ≼ 𝐵 ) |
51 |
5 50
|
mtand |
⊢ ( 𝜑 → ¬ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝐶 = 𝐷 → 𝑥 = 𝑦 ) ) |
52 |
|
ancom |
⊢ ( ( ¬ 𝑥 = 𝑦 ∧ 𝐶 = 𝐷 ) ↔ ( 𝐶 = 𝐷 ∧ ¬ 𝑥 = 𝑦 ) ) |
53 |
|
df-ne |
⊢ ( 𝑥 ≠ 𝑦 ↔ ¬ 𝑥 = 𝑦 ) |
54 |
53
|
anbi1i |
⊢ ( ( 𝑥 ≠ 𝑦 ∧ 𝐶 = 𝐷 ) ↔ ( ¬ 𝑥 = 𝑦 ∧ 𝐶 = 𝐷 ) ) |
55 |
|
pm4.61 |
⊢ ( ¬ ( 𝐶 = 𝐷 → 𝑥 = 𝑦 ) ↔ ( 𝐶 = 𝐷 ∧ ¬ 𝑥 = 𝑦 ) ) |
56 |
52 54 55
|
3bitr4i |
⊢ ( ( 𝑥 ≠ 𝑦 ∧ 𝐶 = 𝐷 ) ↔ ¬ ( 𝐶 = 𝐷 → 𝑥 = 𝑦 ) ) |
57 |
56
|
rexbii |
⊢ ( ∃ 𝑦 ∈ 𝐴 ( 𝑥 ≠ 𝑦 ∧ 𝐶 = 𝐷 ) ↔ ∃ 𝑦 ∈ 𝐴 ¬ ( 𝐶 = 𝐷 → 𝑥 = 𝑦 ) ) |
58 |
|
rexnal |
⊢ ( ∃ 𝑦 ∈ 𝐴 ¬ ( 𝐶 = 𝐷 → 𝑥 = 𝑦 ) ↔ ¬ ∀ 𝑦 ∈ 𝐴 ( 𝐶 = 𝐷 → 𝑥 = 𝑦 ) ) |
59 |
57 58
|
bitri |
⊢ ( ∃ 𝑦 ∈ 𝐴 ( 𝑥 ≠ 𝑦 ∧ 𝐶 = 𝐷 ) ↔ ¬ ∀ 𝑦 ∈ 𝐴 ( 𝐶 = 𝐷 → 𝑥 = 𝑦 ) ) |
60 |
59
|
rexbii |
⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( 𝑥 ≠ 𝑦 ∧ 𝐶 = 𝐷 ) ↔ ∃ 𝑥 ∈ 𝐴 ¬ ∀ 𝑦 ∈ 𝐴 ( 𝐶 = 𝐷 → 𝑥 = 𝑦 ) ) |
61 |
|
rexnal |
⊢ ( ∃ 𝑥 ∈ 𝐴 ¬ ∀ 𝑦 ∈ 𝐴 ( 𝐶 = 𝐷 → 𝑥 = 𝑦 ) ↔ ¬ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝐶 = 𝐷 → 𝑥 = 𝑦 ) ) |
62 |
60 61
|
bitri |
⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( 𝑥 ≠ 𝑦 ∧ 𝐶 = 𝐷 ) ↔ ¬ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝐶 = 𝐷 → 𝑥 = 𝑦 ) ) |
63 |
51 62
|
sylibr |
⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( 𝑥 ≠ 𝑦 ∧ 𝐶 = 𝐷 ) ) |