| Step |
Hyp |
Ref |
Expression |
| 1 |
|
ac6s6.1 |
⊢ Ⅎ 𝑦 𝜓 |
| 2 |
|
ac6s6.2 |
⊢ 𝐴 ∈ V |
| 3 |
|
ac6s6.3 |
⊢ ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) ) |
| 4 |
|
hbe1 |
⊢ ( ∃ 𝑦 𝜑 → ∀ 𝑦 ∃ 𝑦 𝜑 ) |
| 5 |
|
iftrue |
⊢ ( ∃ 𝑦 𝜑 → if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) = { 𝑦 ∣ 𝜑 } ) |
| 6 |
5
|
eqabrd |
⊢ ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) |
| 7 |
4 6
|
exbidh |
⊢ ( ∃ 𝑦 𝜑 → ( ∃ 𝑦 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ∃ 𝑦 𝜑 ) ) |
| 8 |
7
|
ibir |
⊢ ( ∃ 𝑦 𝜑 → ∃ 𝑦 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ) |
| 9 |
|
vex |
⊢ 𝑦 ∈ V |
| 10 |
9
|
exgen |
⊢ ∃ 𝑦 𝑦 ∈ V |
| 11 |
4
|
hbn |
⊢ ( ¬ ∃ 𝑦 𝜑 → ∀ 𝑦 ¬ ∃ 𝑦 𝜑 ) |
| 12 |
|
iffalse |
⊢ ( ¬ ∃ 𝑦 𝜑 → if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) = V ) |
| 13 |
12
|
eleq2d |
⊢ ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝑦 ∈ V ) ) |
| 14 |
11 13
|
exbidh |
⊢ ( ¬ ∃ 𝑦 𝜑 → ( ∃ 𝑦 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ∃ 𝑦 𝑦 ∈ V ) ) |
| 15 |
10 14
|
mpbiri |
⊢ ( ¬ ∃ 𝑦 𝜑 → ∃ 𝑦 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ) |
| 16 |
8 15
|
pm2.61i |
⊢ ∃ 𝑦 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) |
| 17 |
16
|
rgenw |
⊢ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) |
| 18 |
|
nfe1 |
⊢ Ⅎ 𝑦 ∃ 𝑦 𝜑 |
| 19 |
18 1
|
nfim |
⊢ Ⅎ 𝑦 ( ∃ 𝑦 𝜑 → 𝜓 ) |
| 20 |
|
id |
⊢ ( ¬ 𝜑 → ¬ 𝜑 ) |
| 21 |
20
|
a1i |
⊢ ( ¬ ( ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) ) → ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) → ( ¬ 𝜑 → ¬ 𝜑 ) ) |
| 22 |
|
ax-1 |
⊢ ( ¬ ( ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) ) → ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) → ( ¬ 𝜑 → ¬ ( ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) ) → ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) ) ) |
| 23 |
|
tsim3 |
⊢ ( ¬ ( ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) ) → ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) → ( ¬ ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ∨ ( ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) ) → ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) ) ) |
| 24 |
23
|
a1d |
⊢ ( ¬ ( ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) ) → ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) → ( ¬ 𝜑 → ( ¬ ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ∨ ( ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) ) → ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) ) ) ) |
| 25 |
22 24
|
cnf2dd |
⊢ ( ¬ ( ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) ) → ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) → ( ¬ 𝜑 → ¬ ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) ) |
| 26 |
|
tsim3 |
⊢ ( ¬ ( ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) ) → ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) → ( ¬ ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ∨ ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) ) |
| 27 |
26
|
a1d |
⊢ ( ¬ ( ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) ) → ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) → ( ¬ 𝜑 → ( ¬ ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ∨ ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) ) ) |
| 28 |
25 27
|
cnf2dd |
⊢ ( ¬ ( ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) ) → ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) → ( ¬ 𝜑 → ¬ ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) |
| 29 |
|
tsim2 |
⊢ ( ¬ ( ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) ) → ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) → ( ∃ 𝑦 𝜑 ∨ ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) |
| 30 |
29
|
a1d |
⊢ ( ¬ ( ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) ) → ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) → ( ¬ 𝜑 → ( ∃ 𝑦 𝜑 ∨ ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) ) |
| 31 |
28 30
|
cnf2dd |
⊢ ( ¬ ( ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) ) → ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) → ( ¬ 𝜑 → ∃ 𝑦 𝜑 ) ) |
| 32 |
|
tsim2 |
⊢ ( ¬ ( ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) ) → ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) → ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) ∨ ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) ) |
| 33 |
32
|
a1d |
⊢ ( ¬ ( ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) ) → ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) → ( ¬ 𝜑 → ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) ∨ ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) ) ) |
| 34 |
25 33
|
cnf2dd |
⊢ ( ¬ ( ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) ) → ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) → ( ¬ 𝜑 → ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) ) ) |
| 35 |
31 34
|
mpdd |
⊢ ( ¬ ( ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) ) → ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) → ( ¬ 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) ) |
| 36 |
|
tsbi4 |
⊢ ( ¬ ( ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) ) → ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) → ( ( ¬ 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ∨ 𝜑 ) ∨ ¬ ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) ) |
| 37 |
36
|
a1d |
⊢ ( ¬ ( ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) ) → ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) → ( ¬ 𝜑 → ( ( ¬ 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ∨ 𝜑 ) ∨ ¬ ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) ) ) |
| 38 |
35 37
|
cnfn2dd |
⊢ ( ¬ ( ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) ) → ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) → ( ¬ 𝜑 → ( ¬ 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ∨ 𝜑 ) ) ) |
| 39 |
21 38
|
cnf2dd |
⊢ ( ¬ ( ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) ) → ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) → ( ¬ 𝜑 → ¬ 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ) ) |
| 40 |
|
tsim3 |
⊢ ( ¬ ( ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) ) → ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) → ( ¬ ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ∨ ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) |
| 41 |
40
|
a1d |
⊢ ( ¬ ( ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) ) → ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) → ( ¬ 𝜑 → ( ¬ ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ∨ ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) ) |
| 42 |
28 41
|
cnf2dd |
⊢ ( ¬ ( ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) ) → ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) → ( ¬ 𝜑 → ¬ ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) |
| 43 |
|
tsim3 |
⊢ ( ¬ ( ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) ) → ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) → ( ¬ ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ∨ ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) |
| 44 |
43
|
a1d |
⊢ ( ¬ ( ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) ) → ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) → ( ¬ 𝜑 → ( ¬ ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ∨ ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) |
| 45 |
42 44
|
cnf2dd |
⊢ ( ¬ ( ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) ) → ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) → ( ¬ 𝜑 → ¬ ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) |
| 46 |
|
tsbi2 |
⊢ ( ¬ ( ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) ) → ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) → ( ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ∨ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ∨ ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) |
| 47 |
46
|
a1d |
⊢ ( ¬ ( ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) ) → ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) → ( ¬ 𝜑 → ( ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ∨ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ∨ ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) |
| 48 |
45 47
|
cnf2dd |
⊢ ( ¬ ( ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) ) → ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) → ( ¬ 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ∨ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) |
| 49 |
39 48
|
cnf1dd |
⊢ ( ¬ ( ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) ) → ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) → ( ¬ 𝜑 → ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) |
| 50 |
|
tsim2 |
⊢ ( ¬ ( ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) ) → ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) ∨ ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) |
| 51 |
50
|
a1d |
⊢ ( ¬ ( ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) ) → ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) → ( ¬ 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) ∨ ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) |
| 52 |
42 51
|
cnf2dd |
⊢ ( ¬ ( ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) ) → ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) → ( ¬ 𝜑 → 𝑦 = ( 𝑓 ‘ 𝑥 ) ) ) |
| 53 |
|
simplim |
⊢ ( ¬ ( ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) ) → ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) ) ) |
| 54 |
52 53
|
syld |
⊢ ( ¬ ( ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) ) → ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) → ( ¬ 𝜑 → ( 𝜑 ↔ 𝜓 ) ) ) |
| 55 |
|
tsbi3 |
⊢ ( ¬ ( ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) ) → ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) → ( ( 𝜑 ∨ ¬ 𝜓 ) ∨ ¬ ( 𝜑 ↔ 𝜓 ) ) ) |
| 56 |
55
|
a1d |
⊢ ( ¬ ( ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) ) → ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) → ( ¬ 𝜑 → ( ( 𝜑 ∨ ¬ 𝜓 ) ∨ ¬ ( 𝜑 ↔ 𝜓 ) ) ) ) |
| 57 |
54 56
|
cnfn2dd |
⊢ ( ¬ ( ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) ) → ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) → ( ¬ 𝜑 → ( 𝜑 ∨ ¬ 𝜓 ) ) ) |
| 58 |
21 57
|
cnf1dd |
⊢ ( ¬ ( ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) ) → ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) → ( ¬ 𝜑 → ¬ 𝜓 ) ) |
| 59 |
|
tsim1 |
⊢ ( ¬ ( ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) ) → ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) → ( ( ¬ ∃ 𝑦 𝜑 ∨ 𝜓 ) ∨ ¬ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) |
| 60 |
59
|
a1d |
⊢ ( ¬ ( ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) ) → ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) → ( ¬ 𝜑 → ( ( ¬ ∃ 𝑦 𝜑 ∨ 𝜓 ) ∨ ¬ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) |
| 61 |
60
|
or32dd |
⊢ ( ¬ ( ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) ) → ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) → ( ¬ 𝜑 → ( ( ¬ ∃ 𝑦 𝜑 ∨ ¬ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ∨ 𝜓 ) ) ) |
| 62 |
58 61
|
cnf2dd |
⊢ ( ¬ ( ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) ) → ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) → ( ¬ 𝜑 → ( ¬ ∃ 𝑦 𝜑 ∨ ¬ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) |
| 63 |
31 62
|
cnfn1dd |
⊢ ( ¬ ( ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) ) → ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) → ( ¬ 𝜑 → ¬ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) |
| 64 |
49 63
|
contrd |
⊢ ( ¬ ( ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) ) → ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) → 𝜑 ) |
| 65 |
64
|
a1d |
⊢ ( ¬ ( ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) ) → ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) → ( ¬ ⊥ → 𝜑 ) ) |
| 66 |
|
ax-1 |
⊢ ( ¬ ( ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) ) → ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) → ( ¬ ⊥ → ¬ ( ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) ) → ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) ) ) |
| 67 |
23
|
a1d |
⊢ ( ¬ ( ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) ) → ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) → ( ¬ ⊥ → ( ¬ ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ∨ ( ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) ) → ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) ) ) ) |
| 68 |
66 67
|
cnf2dd |
⊢ ( ¬ ( ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) ) → ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) → ( ¬ ⊥ → ¬ ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) ) |
| 69 |
26
|
a1d |
⊢ ( ¬ ( ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) ) → ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) → ( ¬ ⊥ → ( ¬ ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ∨ ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) ) ) |
| 70 |
68 69
|
cnf2dd |
⊢ ( ¬ ( ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) ) → ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) → ( ¬ ⊥ → ¬ ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) |
| 71 |
29
|
a1d |
⊢ ( ¬ ( ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) ) → ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) → ( ¬ ⊥ → ( ∃ 𝑦 𝜑 ∨ ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) ) |
| 72 |
70 71
|
cnf2dd |
⊢ ( ¬ ( ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) ) → ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) → ( ¬ ⊥ → ∃ 𝑦 𝜑 ) ) |
| 73 |
32
|
a1d |
⊢ ( ¬ ( ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) ) → ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) → ( ¬ ⊥ → ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) ∨ ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) ) ) |
| 74 |
68 73
|
cnf2dd |
⊢ ( ¬ ( ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) ) → ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) → ( ¬ ⊥ → ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) ) ) |
| 75 |
72 74
|
mpdd |
⊢ ( ¬ ( ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) ) → ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) → ( ¬ ⊥ → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) ) |
| 76 |
|
tsbi3 |
⊢ ( ¬ ( ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) ) → ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) → ( ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ∨ ¬ 𝜑 ) ∨ ¬ ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) ) |
| 77 |
76
|
a1d |
⊢ ( ¬ ( ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) ) → ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) → ( ¬ ⊥ → ( ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ∨ ¬ 𝜑 ) ∨ ¬ ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) ) ) |
| 78 |
75 77
|
cnfn2dd |
⊢ ( ¬ ( ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) ) → ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) → ( ¬ ⊥ → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ∨ ¬ 𝜑 ) ) ) |
| 79 |
65 78
|
cnfn2dd |
⊢ ( ¬ ( ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) ) → ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) → ( ¬ ⊥ → 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ) ) |
| 80 |
40
|
a1d |
⊢ ( ¬ ( ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) ) → ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) → ( ¬ ⊥ → ( ¬ ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ∨ ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) ) |
| 81 |
70 80
|
cnf2dd |
⊢ ( ¬ ( ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) ) → ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) → ( ¬ ⊥ → ¬ ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) |
| 82 |
50
|
a1d |
⊢ ( ¬ ( ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) ) → ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) → ( ¬ ⊥ → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) ∨ ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) |
| 83 |
81 82
|
cnf2dd |
⊢ ( ¬ ( ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) ) → ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) → ( ¬ ⊥ → 𝑦 = ( 𝑓 ‘ 𝑥 ) ) ) |
| 84 |
83 53
|
syld |
⊢ ( ¬ ( ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) ) → ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) → ( ¬ ⊥ → ( 𝜑 ↔ 𝜓 ) ) ) |
| 85 |
|
tsbi4 |
⊢ ( ¬ ( ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) ) → ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) → ( ( ¬ 𝜑 ∨ 𝜓 ) ∨ ¬ ( 𝜑 ↔ 𝜓 ) ) ) |
| 86 |
85
|
a1d |
⊢ ( ¬ ( ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) ) → ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) → ( ¬ ⊥ → ( ( ¬ 𝜑 ∨ 𝜓 ) ∨ ¬ ( 𝜑 ↔ 𝜓 ) ) ) ) |
| 87 |
84 86
|
cnfn2dd |
⊢ ( ¬ ( ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) ) → ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) → ( ¬ ⊥ → ( ¬ 𝜑 ∨ 𝜓 ) ) ) |
| 88 |
65 87
|
cnfn1dd |
⊢ ( ¬ ( ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) ) → ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) → ( ¬ ⊥ → 𝜓 ) ) |
| 89 |
88
|
a1dd |
⊢ ( ¬ ( ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) ) → ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) → ( ¬ ⊥ → ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) |
| 90 |
|
tsbi1 |
⊢ ( ¬ ( ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) ) → ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) → ( ( ¬ 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ∨ ¬ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ∨ ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) |
| 91 |
90
|
a1d |
⊢ ( ¬ ( ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) ) → ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) → ( ¬ ⊥ → ( ( ¬ 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ∨ ¬ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ∨ ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) |
| 92 |
91
|
or32dd |
⊢ ( ¬ ( ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) ) → ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) → ( ¬ ⊥ → ( ( ¬ 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ∨ ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ∨ ¬ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) |
| 93 |
89 92
|
cnfn2dd |
⊢ ( ¬ ( ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) ) → ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) → ( ¬ ⊥ → ( ¬ 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ∨ ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) |
| 94 |
79 93
|
cnfn1dd |
⊢ ( ¬ ( ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) ) → ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) → ( ¬ ⊥ → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) |
| 95 |
43
|
a1d |
⊢ ( ¬ ( ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) ) → ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) → ( ¬ ⊥ → ( ¬ ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ∨ ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) |
| 96 |
81 95
|
cnf2dd |
⊢ ( ¬ ( ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) ) → ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) → ( ¬ ⊥ → ¬ ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) |
| 97 |
94 96
|
contrd |
⊢ ( ¬ ( ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) ) → ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) → ⊥ ) |
| 98 |
97
|
efald2 |
⊢ ( ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝜑 ↔ 𝜓 ) ) → ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) |
| 99 |
3 98
|
ax-mp |
⊢ ( ( ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝜑 ) ) → ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) |
| 100 |
6 99
|
ax-mp |
⊢ ( ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) |
| 101 |
9
|
a1i |
⊢ ( ¬ ∃ 𝑦 𝜑 → 𝑦 ∈ V ) |
| 102 |
|
id |
⊢ ( ¬ ( ( ¬ ∃ 𝑦 𝜑 → 𝑦 ∈ V ) → ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝑦 ∈ V ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) ) ) → ¬ ( ( ¬ ∃ 𝑦 𝜑 → 𝑦 ∈ V ) → ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝑦 ∈ V ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) ) ) ) |
| 103 |
|
tsim2 |
⊢ ( ¬ ( ( ¬ ∃ 𝑦 𝜑 → 𝑦 ∈ V ) → ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝑦 ∈ V ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) ) ) → ( ¬ ∃ 𝑦 𝜑 ∨ ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) ) ) |
| 104 |
103
|
ord |
⊢ ( ¬ ( ( ¬ ∃ 𝑦 𝜑 → 𝑦 ∈ V ) → ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝑦 ∈ V ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) ) ) → ( ¬ ¬ ∃ 𝑦 𝜑 → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) ) ) |
| 105 |
104
|
a1dd |
⊢ ( ¬ ( ( ¬ ∃ 𝑦 𝜑 → 𝑦 ∈ V ) → ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝑦 ∈ V ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) ) ) → ( ¬ ¬ ∃ 𝑦 𝜑 → ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝑦 ∈ V ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) ) ) ) |
| 106 |
105
|
a1dd |
⊢ ( ¬ ( ( ¬ ∃ 𝑦 𝜑 → 𝑦 ∈ V ) → ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝑦 ∈ V ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) ) ) → ( ¬ ¬ ∃ 𝑦 𝜑 → ( ( ¬ ∃ 𝑦 𝜑 → 𝑦 ∈ V ) → ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝑦 ∈ V ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) ) ) ) ) |
| 107 |
102 106
|
mt3d |
⊢ ( ¬ ( ( ¬ ∃ 𝑦 𝜑 → 𝑦 ∈ V ) → ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝑦 ∈ V ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) ) ) → ¬ ∃ 𝑦 𝜑 ) |
| 108 |
107
|
a1d |
⊢ ( ¬ ( ( ¬ ∃ 𝑦 𝜑 → 𝑦 ∈ V ) → ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝑦 ∈ V ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) ) ) → ( ¬ ⊥ → ¬ ∃ 𝑦 𝜑 ) ) |
| 109 |
|
simplim |
⊢ ( ¬ ( ( ¬ ∃ 𝑦 𝜑 → 𝑦 ∈ V ) → ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝑦 ∈ V ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) ) ) → ( ¬ ∃ 𝑦 𝜑 → 𝑦 ∈ V ) ) |
| 110 |
108 109
|
syld |
⊢ ( ¬ ( ( ¬ ∃ 𝑦 𝜑 → 𝑦 ∈ V ) → ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝑦 ∈ V ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) ) ) → ( ¬ ⊥ → 𝑦 ∈ V ) ) |
| 111 |
|
tsim2 |
⊢ ( ¬ ( ( ¬ ∃ 𝑦 𝜑 → 𝑦 ∈ V ) → ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝑦 ∈ V ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) ) ) → ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝑦 ∈ V ) ) ∨ ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝑦 ∈ V ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) ) ) ) |
| 112 |
111
|
ord |
⊢ ( ¬ ( ( ¬ ∃ 𝑦 𝜑 → 𝑦 ∈ V ) → ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝑦 ∈ V ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) ) ) → ( ¬ ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝑦 ∈ V ) ) → ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝑦 ∈ V ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) ) ) ) |
| 113 |
112
|
a1dd |
⊢ ( ¬ ( ( ¬ ∃ 𝑦 𝜑 → 𝑦 ∈ V ) → ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝑦 ∈ V ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) ) ) → ( ¬ ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝑦 ∈ V ) ) → ( ( ¬ ∃ 𝑦 𝜑 → 𝑦 ∈ V ) → ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝑦 ∈ V ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) ) ) ) ) |
| 114 |
102 113
|
mt3d |
⊢ ( ¬ ( ( ¬ ∃ 𝑦 𝜑 → 𝑦 ∈ V ) → ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝑦 ∈ V ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝑦 ∈ V ) ) ) |
| 115 |
108 114
|
syld |
⊢ ( ¬ ( ( ¬ ∃ 𝑦 𝜑 → 𝑦 ∈ V ) → ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝑦 ∈ V ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) ) ) → ( ¬ ⊥ → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝑦 ∈ V ) ) ) |
| 116 |
|
id |
⊢ ( ¬ ( ¬ ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝑦 ∈ V ) ∨ ¬ 𝑦 ∈ V ) → ¬ ( ¬ ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝑦 ∈ V ) ∨ ¬ 𝑦 ∈ V ) ) |
| 117 |
116
|
notornotel2 |
⊢ ( ¬ ( ¬ ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝑦 ∈ V ) ∨ ¬ 𝑦 ∈ V ) → 𝑦 ∈ V ) |
| 118 |
117
|
a1i |
⊢ ( ¬ ( ( ¬ ∃ 𝑦 𝜑 → 𝑦 ∈ V ) → ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝑦 ∈ V ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) ) ) → ( ¬ ( ¬ ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝑦 ∈ V ) ∨ ¬ 𝑦 ∈ V ) → 𝑦 ∈ V ) ) |
| 119 |
116
|
notornotel1 |
⊢ ( ¬ ( ¬ ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝑦 ∈ V ) ∨ ¬ 𝑦 ∈ V ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝑦 ∈ V ) ) |
| 120 |
119
|
a1i |
⊢ ( ¬ ( ( ¬ ∃ 𝑦 𝜑 → 𝑦 ∈ V ) → ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝑦 ∈ V ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) ) ) → ( ¬ ( ¬ ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝑦 ∈ V ) ∨ ¬ 𝑦 ∈ V ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝑦 ∈ V ) ) ) |
| 121 |
|
tsbi3 |
⊢ ( ¬ ( ( ¬ ∃ 𝑦 𝜑 → 𝑦 ∈ V ) → ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝑦 ∈ V ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) ) ) → ( ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ∨ ¬ 𝑦 ∈ V ) ∨ ¬ ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝑦 ∈ V ) ) ) |
| 122 |
121
|
a1d |
⊢ ( ¬ ( ( ¬ ∃ 𝑦 𝜑 → 𝑦 ∈ V ) → ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝑦 ∈ V ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) ) ) → ( ¬ ( ¬ ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝑦 ∈ V ) ∨ ¬ 𝑦 ∈ V ) → ( ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ∨ ¬ 𝑦 ∈ V ) ∨ ¬ ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝑦 ∈ V ) ) ) ) |
| 123 |
120 122
|
cnfn2dd |
⊢ ( ¬ ( ( ¬ ∃ 𝑦 𝜑 → 𝑦 ∈ V ) → ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝑦 ∈ V ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) ) ) → ( ¬ ( ¬ ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝑦 ∈ V ) ∨ ¬ 𝑦 ∈ V ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ∨ ¬ 𝑦 ∈ V ) ) ) |
| 124 |
118 123
|
cnfn2dd |
⊢ ( ¬ ( ( ¬ ∃ 𝑦 𝜑 → 𝑦 ∈ V ) → ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝑦 ∈ V ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) ) ) → ( ¬ ( ¬ ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝑦 ∈ V ) ∨ ¬ 𝑦 ∈ V ) → 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ) ) |
| 125 |
|
trud |
⊢ ( ¬ ( ( ¬ ∃ 𝑦 𝜑 → 𝑦 ∈ V ) → ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝑦 ∈ V ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) ) ) → ⊤ ) |
| 126 |
125
|
a1d |
⊢ ( ¬ ( ( ¬ ∃ 𝑦 𝜑 → 𝑦 ∈ V ) → ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝑦 ∈ V ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) ) ) → ( ¬ ( ¬ ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝑦 ∈ V ) ∨ ¬ 𝑦 ∈ V ) → ⊤ ) ) |
| 127 |
|
tsbi1 |
⊢ ( ¬ ( ( ¬ ∃ 𝑦 𝜑 → 𝑦 ∈ V ) → ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝑦 ∈ V ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) ) ) → ( ( ¬ 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ∨ ¬ ⊤ ) ∨ ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) ) |
| 128 |
127
|
a1d |
⊢ ( ¬ ( ( ¬ ∃ 𝑦 𝜑 → 𝑦 ∈ V ) → ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝑦 ∈ V ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) ) ) → ( ¬ ( ¬ ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝑦 ∈ V ) ∨ ¬ 𝑦 ∈ V ) → ( ( ¬ 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ∨ ¬ ⊤ ) ∨ ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) ) ) |
| 129 |
128
|
or32dd |
⊢ ( ¬ ( ( ¬ ∃ 𝑦 𝜑 → 𝑦 ∈ V ) → ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝑦 ∈ V ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) ) ) → ( ¬ ( ¬ ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝑦 ∈ V ) ∨ ¬ 𝑦 ∈ V ) → ( ( ¬ 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ∨ ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) ∨ ¬ ⊤ ) ) ) |
| 130 |
126 129
|
cnfn2dd |
⊢ ( ¬ ( ( ¬ ∃ 𝑦 𝜑 → 𝑦 ∈ V ) → ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝑦 ∈ V ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) ) ) → ( ¬ ( ¬ ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝑦 ∈ V ) ∨ ¬ 𝑦 ∈ V ) → ( ¬ 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ∨ ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) ) ) |
| 131 |
124 130
|
cnfn1dd |
⊢ ( ¬ ( ( ¬ ∃ 𝑦 𝜑 → 𝑦 ∈ V ) → ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝑦 ∈ V ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) ) ) → ( ¬ ( ¬ ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝑦 ∈ V ) ∨ ¬ 𝑦 ∈ V ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) ) |
| 132 |
131
|
a1dd |
⊢ ( ¬ ( ( ¬ ∃ 𝑦 𝜑 → 𝑦 ∈ V ) → ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝑦 ∈ V ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) ) ) → ( ¬ ( ¬ ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝑦 ∈ V ) ∨ ¬ 𝑦 ∈ V ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) ) ) |
| 133 |
132
|
a1dd |
⊢ ( ¬ ( ( ¬ ∃ 𝑦 𝜑 → 𝑦 ∈ V ) → ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝑦 ∈ V ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) ) ) → ( ¬ ( ¬ ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝑦 ∈ V ) ∨ ¬ 𝑦 ∈ V ) → ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝑦 ∈ V ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) ) ) ) |
| 134 |
|
ax-1 |
⊢ ( ¬ ( ( ¬ ∃ 𝑦 𝜑 → 𝑦 ∈ V ) → ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝑦 ∈ V ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) ) ) → ( ¬ ( ¬ ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝑦 ∈ V ) ∨ ¬ 𝑦 ∈ V ) → ¬ ( ( ¬ ∃ 𝑦 𝜑 → 𝑦 ∈ V ) → ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝑦 ∈ V ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) ) ) ) ) |
| 135 |
|
tsim3 |
⊢ ( ¬ ( ( ¬ ∃ 𝑦 𝜑 → 𝑦 ∈ V ) → ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝑦 ∈ V ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) ) ) → ( ¬ ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝑦 ∈ V ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) ) ∨ ( ( ¬ ∃ 𝑦 𝜑 → 𝑦 ∈ V ) → ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝑦 ∈ V ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) ) ) ) ) |
| 136 |
135
|
a1d |
⊢ ( ¬ ( ( ¬ ∃ 𝑦 𝜑 → 𝑦 ∈ V ) → ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝑦 ∈ V ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) ) ) → ( ¬ ( ¬ ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝑦 ∈ V ) ∨ ¬ 𝑦 ∈ V ) → ( ¬ ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝑦 ∈ V ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) ) ∨ ( ( ¬ ∃ 𝑦 𝜑 → 𝑦 ∈ V ) → ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝑦 ∈ V ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) ) ) ) ) ) |
| 137 |
134 136
|
cnf2dd |
⊢ ( ¬ ( ( ¬ ∃ 𝑦 𝜑 → 𝑦 ∈ V ) → ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝑦 ∈ V ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) ) ) → ( ¬ ( ¬ ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝑦 ∈ V ) ∨ ¬ 𝑦 ∈ V ) → ¬ ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝑦 ∈ V ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) ) ) ) |
| 138 |
133 137
|
contrd |
⊢ ( ¬ ( ( ¬ ∃ 𝑦 𝜑 → 𝑦 ∈ V ) → ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝑦 ∈ V ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) ) ) → ( ¬ ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝑦 ∈ V ) ∨ ¬ 𝑦 ∈ V ) ) |
| 139 |
138
|
a1d |
⊢ ( ¬ ( ( ¬ ∃ 𝑦 𝜑 → 𝑦 ∈ V ) → ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝑦 ∈ V ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) ) ) → ( ¬ ⊥ → ( ¬ ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝑦 ∈ V ) ∨ ¬ 𝑦 ∈ V ) ) ) |
| 140 |
115 139
|
cnfn1dd |
⊢ ( ¬ ( ( ¬ ∃ 𝑦 𝜑 → 𝑦 ∈ V ) → ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝑦 ∈ V ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) ) ) → ( ¬ ⊥ → ¬ 𝑦 ∈ V ) ) |
| 141 |
110 140
|
contrd |
⊢ ( ¬ ( ( ¬ ∃ 𝑦 𝜑 → 𝑦 ∈ V ) → ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝑦 ∈ V ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) ) ) → ⊥ ) |
| 142 |
141
|
efald2 |
⊢ ( ( ¬ ∃ 𝑦 𝜑 → 𝑦 ∈ V ) → ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝑦 ∈ V ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) ) ) |
| 143 |
101 142
|
ax-mp |
⊢ ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ 𝑦 ∈ V ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) ) |
| 144 |
13 143
|
ax-mp |
⊢ ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) |
| 145 |
|
ax-1 |
⊢ ( ¬ ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) → ( ¬ ⊥ → ¬ ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) ) |
| 146 |
|
tsim3 |
⊢ ( ¬ ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) → ( ¬ ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ∨ ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) ) |
| 147 |
146
|
a1d |
⊢ ( ¬ ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) → ( ¬ ⊥ → ( ¬ ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ∨ ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) ) ) |
| 148 |
145 147
|
cnf2dd |
⊢ ( ¬ ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) → ( ¬ ⊥ → ¬ ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) |
| 149 |
|
tsim2 |
⊢ ( ¬ ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) → ( ¬ ∃ 𝑦 𝜑 ∨ ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) |
| 150 |
149
|
a1d |
⊢ ( ¬ ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) → ( ¬ ⊥ → ( ¬ ∃ 𝑦 𝜑 ∨ ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) ) |
| 151 |
148 150
|
cnf2dd |
⊢ ( ¬ ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) → ( ¬ ⊥ → ¬ ∃ 𝑦 𝜑 ) ) |
| 152 |
|
tsim2 |
⊢ ( ¬ ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) → ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) ∨ ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) ) |
| 153 |
152
|
a1d |
⊢ ( ¬ ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) → ( ¬ ⊥ → ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) ∨ ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) ) ) |
| 154 |
145 153
|
cnf2dd |
⊢ ( ¬ ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) → ( ¬ ⊥ → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) ) ) |
| 155 |
151 154
|
mpdd |
⊢ ( ¬ ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) → ( ¬ ⊥ → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) ) |
| 156 |
|
id |
⊢ ( ¬ ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) → ¬ ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) |
| 157 |
|
id |
⊢ ( ¬ ( ∃ 𝑦 𝜑 → 𝜓 ) → ¬ ( ∃ 𝑦 𝜑 → 𝜓 ) ) |
| 158 |
157
|
a1i |
⊢ ( ¬ ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) → ( ¬ ( ∃ 𝑦 𝜑 → 𝜓 ) → ¬ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) |
| 159 |
|
tsim2 |
⊢ ( ¬ ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) → ( ∃ 𝑦 𝜑 ∨ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) |
| 160 |
159
|
a1d |
⊢ ( ¬ ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) → ( ¬ ( ∃ 𝑦 𝜑 → 𝜓 ) → ( ∃ 𝑦 𝜑 ∨ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) |
| 161 |
158 160
|
cnf2dd |
⊢ ( ¬ ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) → ( ¬ ( ∃ 𝑦 𝜑 → 𝜓 ) → ∃ 𝑦 𝜑 ) ) |
| 162 |
149
|
a1d |
⊢ ( ¬ ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) → ( ¬ ( ∃ 𝑦 𝜑 → 𝜓 ) → ( ¬ ∃ 𝑦 𝜑 ∨ ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) ) |
| 163 |
161 162
|
cnfn1dd |
⊢ ( ¬ ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) → ( ¬ ( ∃ 𝑦 𝜑 → 𝜓 ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) |
| 164 |
163
|
a1dd |
⊢ ( ¬ ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) → ( ¬ ( ∃ 𝑦 𝜑 → 𝜓 ) → ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) ) |
| 165 |
156 164
|
mt3d |
⊢ ( ¬ ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) → ( ∃ 𝑦 𝜑 → 𝜓 ) ) |
| 166 |
165
|
a1d |
⊢ ( ¬ ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) → ( ¬ ⊥ → ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) |
| 167 |
|
tsim3 |
⊢ ( ¬ ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) → ( ¬ ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ∨ ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) |
| 168 |
167
|
a1d |
⊢ ( ¬ ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) → ( ¬ ⊥ → ( ¬ ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ∨ ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) ) |
| 169 |
148 168
|
cnf2dd |
⊢ ( ¬ ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) → ( ¬ ⊥ → ¬ ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) |
| 170 |
|
tsim3 |
⊢ ( ¬ ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) → ( ¬ ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ∨ ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) |
| 171 |
170
|
a1d |
⊢ ( ¬ ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) → ( ¬ ⊥ → ( ¬ ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ∨ ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) ) |
| 172 |
169 171
|
cnf2dd |
⊢ ( ¬ ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) → ( ¬ ⊥ → ¬ ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) |
| 173 |
|
tsbi1 |
⊢ ( ¬ ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) → ( ( ¬ 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ∨ ¬ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ∨ ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) |
| 174 |
173
|
a1d |
⊢ ( ¬ ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) → ( ¬ ⊥ → ( ( ¬ 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ∨ ¬ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ∨ ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) |
| 175 |
172 174
|
cnf2dd |
⊢ ( ¬ ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) → ( ¬ ⊥ → ( ¬ 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ∨ ¬ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) |
| 176 |
166 175
|
cnfn2dd |
⊢ ( ¬ ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) → ( ¬ ⊥ → ¬ 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ) ) |
| 177 |
|
trud |
⊢ ( ¬ ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) → ⊤ ) |
| 178 |
177
|
a1d |
⊢ ( ¬ ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) → ( ¬ ⊥ → ⊤ ) ) |
| 179 |
|
tsbi3 |
⊢ ( ¬ ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) → ( ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ∨ ¬ ⊤ ) ∨ ¬ ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) ) |
| 180 |
179
|
a1d |
⊢ ( ¬ ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) → ( ¬ ⊥ → ( ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ∨ ¬ ⊤ ) ∨ ¬ ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) ) ) |
| 181 |
180
|
or32dd |
⊢ ( ¬ ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) → ( ¬ ⊥ → ( ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ∨ ¬ ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) ∨ ¬ ⊤ ) ) ) |
| 182 |
178 181
|
cnfn2dd |
⊢ ( ¬ ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) → ( ¬ ⊥ → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ∨ ¬ ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) ) ) |
| 183 |
176 182
|
cnf1dd |
⊢ ( ¬ ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) → ( ¬ ⊥ → ¬ ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) ) |
| 184 |
155 183
|
contrd |
⊢ ( ¬ ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) → ⊥ ) |
| 185 |
184
|
efald2 |
⊢ ( ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ⊤ ) ) → ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) ) |
| 186 |
144 185
|
ax-mp |
⊢ ( ¬ ∃ 𝑦 𝜑 → ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) ) |
| 187 |
100 186
|
pm2.61i |
⊢ ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) ↔ ( ∃ 𝑦 𝜑 → 𝜓 ) ) ) |
| 188 |
19 2 187
|
ac6s3f |
⊢ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 𝑦 ∈ if ( ∃ 𝑦 𝜑 , { 𝑦 ∣ 𝜑 } , V ) → ∃ 𝑓 ∀ 𝑥 ∈ 𝐴 ( ∃ 𝑦 𝜑 → 𝜓 ) ) |
| 189 |
17 188
|
ax-mp |
⊢ ∃ 𝑓 ∀ 𝑥 ∈ 𝐴 ( ∃ 𝑦 𝜑 → 𝜓 ) |