Users' Mathboxes Mathbox for Giovanni Mascellani < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ac6s6 Structured version   Visualization version   GIF version
Theorem ac6s6 39247
Description: Generalization of the Axiom of Choice to classes, moving the existence condition in the consequent. (Contributed by Giovanni Mascellani, 19-Aug-2018.)
Hypotheses
Ref Expression
ac6s6.1 Ⅎ𝑦𝜓
ac6s6.2 𝐴 ∈ V
ac6s6.3 (𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓))
Assertion
Ref Expression
ac6s6 ∃𝑓∀𝑥 ∈ 𝐴 (∃𝑦𝜑 → 𝜓)
Distinct variable groups:   𝜑,𝑓   𝑥,𝑦   𝑥,𝐴,𝑓   𝑦,𝑓   𝐴,𝑓
Allowed substitution hints:   𝜑(𝑥, 𝑦)   𝜓(𝑥, 𝑦, 𝑓)   𝐴(𝑦)
Proof of Theorem ac6s6
StepHypRef Expression
1 hbe1 2181 . . . . . 6 (∃𝑦𝜑 → ∀𝑦∃𝑦𝜑)
2 iftrue 4491 . . . . . . 7 (∃𝑦𝜑 → if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) = {𝑦 ∣ 𝜑})
32eqabrd 2905 . . . . . 6 (∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑))
41, 3exbidh 1899 . . . . 5 (∃𝑦𝜑 → (∃𝑦 𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ∃𝑦𝜑))
54ibir 271 . . . 4 (∃𝑦𝜑 → ∃𝑦 𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V))
6 vex 3458 . . . . . 6 𝑦 ∈ V
76exgen 2008 . . . . 5 ∃𝑦 𝑦 ∈ V
81hbn 2331 . . . . . 6 (¬ ∃𝑦𝜑 → ∀𝑦 ¬ ∃𝑦𝜑)
9 iffalse 4494 . . . . . . 7 (¬ ∃𝑦𝜑 → if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) = V)
109eleq2d 2850 . . . . . 6 (¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝑦 ∈ V))
118, 10exbidh 1899 . . . . 5 (¬ ∃𝑦𝜑 → (∃𝑦 𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ∃𝑦 𝑦 ∈ V))
127, 11mpbiri 261 . . . 4 (¬ ∃𝑦𝜑 → ∃𝑦 𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V))
135, 12pm2.61i 184 . . 3 ∃𝑦 𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V)
1413rgenw 3084 . 2 ∀𝑥 ∈ 𝐴 ∃𝑦 𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V)
15 nfe1 2189 . . . 4 Ⅎ𝑦∃𝑦𝜑
16 ac6s6.1 . . . 4 Ⅎ𝑦𝜓
1715, 16nfim 1930 . . 3 Ⅎ𝑦(∃𝑦𝜑 → 𝜓)
18 ac6s6.2 . . 3 𝐴 ∈ V
19 ac6s6.3 . . . . . 6 (𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓))
20 id 23 . . . . . . . . . . . . . . 15 (¬ 𝜑 → ¬ 𝜑)
2120a1i 11 . . . . . . . . . . . . . 14 (¬ ((𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) → ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))) → (¬ 𝜑 → ¬ 𝜑))
22 ax-1 6 . . . . . . . . . . . . . . . . . . 19 (¬ ((𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) → ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))) → (¬ 𝜑 → ¬ ((𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) → ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓))))))))
23 tsim3 39207 . . . . . . . . . . . . . . . . . . . 20 (¬ ((𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) → ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))) → (¬ ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓))))) ∨ ((𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) → ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓))))))))
2423a1d 26 . . . . . . . . . . . . . . . . . . 19 (¬ ((𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) → ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))) → (¬ 𝜑 → (¬ ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓))))) ∨ ((𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) → ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))))))
2522, 24cnf2dd 39166 . . . . . . . . . . . . . . . . . 18 (¬ ((𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) → ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))) → (¬ 𝜑 → ¬ ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))))
26 tsim3 39207 . . . . . . . . . . . . . . . . . . 19 (¬ ((𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) → ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))) → (¬ (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))) ∨ ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))))
2726a1d 26 . . . . . . . . . . . . . . . . . 18 (¬ ((𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) → ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))) → (¬ 𝜑 → (¬ (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))) ∨ ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓))))))))
2825, 27cnf2dd 39166 . . . . . . . . . . . . . . . . 17 (¬ ((𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) → ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))) → (¬ 𝜑 → ¬ (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓))))))
29 tsim2 39206 . . . . . . . . . . . . . . . . . 18 (¬ ((𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) → ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))) → (∃𝑦𝜑 ∨ (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓))))))
3029a1d 26 . . . . . . . . . . . . . . . . 17 (¬ ((𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) → ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))) → (¬ 𝜑 → (∃𝑦𝜑 ∨ (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))))
3128, 30cnf2dd 39166 . . . . . . . . . . . . . . . 16 (¬ ((𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) → ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))) → (¬ 𝜑 → ∃𝑦𝜑))
32 tsim2 39206 . . . . . . . . . . . . . . . . . 18 (¬ ((𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) → ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))) → ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) ∨ ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))))
3332a1d 26 . . . . . . . . . . . . . . . . 17 (¬ ((𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) → ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))) → (¬ 𝜑 → ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) ∨ ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓))))))))
3425, 33cnf2dd 39166 . . . . . . . . . . . . . . . 16 (¬ ((𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) → ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))) → (¬ 𝜑 → (∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑))))
3531, 34mpdd 44 . . . . . . . . . . . . . . 15 (¬ ((𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) → ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))) → (¬ 𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)))
36 tsbi4 39211 . . . . . . . . . . . . . . . 16 (¬ ((𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) → ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))) → ((¬ 𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ∨ 𝜑) ∨ ¬ (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)))
3736a1d 26 . . . . . . . . . . . . . . 15 (¬ ((𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) → ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))) → (¬ 𝜑 → ((¬ 𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ∨ 𝜑) ∨ ¬ (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑))))
3835, 37cnfn2dd 39168 . . . . . . . . . . . . . 14 (¬ ((𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) → ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))) → (¬ 𝜑 → (¬ 𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ∨ 𝜑)))
3921, 38cnf2dd 39166 . . . . . . . . . . . . 13 (¬ ((𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) → ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))) → (¬ 𝜑 → ¬ 𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V)))
40 tsim3 39207 . . . . . . . . . . . . . . . . 17 (¬ ((𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) → ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))) → (¬ (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓))) ∨ (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓))))))
4140a1d 26 . . . . . . . . . . . . . . . 16 (¬ ((𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) → ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))) → (¬ 𝜑 → (¬ (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓))) ∨ (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))))
4228, 41cnf2dd 39166 . . . . . . . . . . . . . . 15 (¬ ((𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) → ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))) → (¬ 𝜑 → ¬ (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))
43 tsim3 39207 . . . . . . . . . . . . . . . 16 (¬ ((𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) → ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))) → (¬ (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)) ∨ (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))
4443a1d 26 . . . . . . . . . . . . . . 15 (¬ ((𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) → ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))) → (¬ 𝜑 → (¬ (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)) ∨ (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓))))))
4542, 44cnf2dd 39166 . . . . . . . . . . . . . 14 (¬ ((𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) → ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))) → (¬ 𝜑 → ¬ (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓))))
46 tsbi2 39209 . . . . . . . . . . . . . . 15 (¬ ((𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) → ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))) → ((𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ∨ (∃𝑦𝜑 → 𝜓)) ∨ (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓))))
4746a1d 26 . . . . . . . . . . . . . 14 (¬ ((𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) → ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))) → (¬ 𝜑 → ((𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ∨ (∃𝑦𝜑 → 𝜓)) ∨ (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))
4845, 47cnf2dd 39166 . . . . . . . . . . . . 13 (¬ ((𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) → ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))) → (¬ 𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ∨ (∃𝑦𝜑 → 𝜓))))
4939, 48cnf1dd 39165 . . . . . . . . . . . 12 (¬ ((𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) → ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))) → (¬ 𝜑 → (∃𝑦𝜑 → 𝜓)))
50 tsim2 39206 . . . . . . . . . . . . . . . . . . 19 (¬ ((𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) → ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))) → (𝑦 = (𝑓‘𝑥) ∨ (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))
5150a1d 26 . . . . . . . . . . . . . . . . . 18 (¬ ((𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) → ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))) → (¬ 𝜑 → (𝑦 = (𝑓‘𝑥) ∨ (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓))))))
5242, 51cnf2dd 39166 . . . . . . . . . . . . . . . . 17 (¬ ((𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) → ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))) → (¬ 𝜑 → 𝑦 = (𝑓‘𝑥)))
53 simplim 168 . . . . . . . . . . . . . . . . 17 (¬ ((𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) → ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))) → (𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)))
5452, 53syld 48 . . . . . . . . . . . . . . . 16 (¬ ((𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) → ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))) → (¬ 𝜑 → (𝜑 ↔ 𝜓)))
55 tsbi3 39210 . . . . . . . . . . . . . . . . 17 (¬ ((𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) → ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))) → ((𝜑 ∨ ¬ 𝜓) ∨ ¬ (𝜑 ↔ 𝜓)))
5655a1d 26 . . . . . . . . . . . . . . . 16 (¬ ((𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) → ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))) → (¬ 𝜑 → ((𝜑 ∨ ¬ 𝜓) ∨ ¬ (𝜑 ↔ 𝜓))))
5754, 56cnfn2dd 39168 . . . . . . . . . . . . . . 15 (¬ ((𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) → ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))) → (¬ 𝜑 → (𝜑 ∨ ¬ 𝜓)))
5821, 57cnf1dd 39165 . . . . . . . . . . . . . 14 (¬ ((𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) → ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))) → (¬ 𝜑 → ¬ 𝜓))
59 tsim1 39205 . . . . . . . . . . . . . . . 16 (¬ ((𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) → ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))) → ((¬ ∃𝑦𝜑 ∨ 𝜓) ∨ ¬ (∃𝑦𝜑 → 𝜓)))
6059a1d 26 . . . . . . . . . . . . . . 15 (¬ ((𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) → ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))) → (¬ 𝜑 → ((¬ ∃𝑦𝜑 ∨ 𝜓) ∨ ¬ (∃𝑦𝜑 → 𝜓))))
6160or32dd 39169 . . . . . . . . . . . . . 14 (¬ ((𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) → ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))) → (¬ 𝜑 → ((¬ ∃𝑦𝜑 ∨ ¬ (∃𝑦𝜑 → 𝜓)) ∨ 𝜓)))
6258, 61cnf2dd 39166 . . . . . . . . . . . . 13 (¬ ((𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) → ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))) → (¬ 𝜑 → (¬ ∃𝑦𝜑 ∨ ¬ (∃𝑦𝜑 → 𝜓))))
6331, 62cnfn1dd 39167 . . . . . . . . . . . 12 (¬ ((𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) → ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))) → (¬ 𝜑 → ¬ (∃𝑦𝜑 → 𝜓)))
6449, 63contrd 39172 . . . . . . . . . . 11 (¬ ((𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) → ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))) → 𝜑)
6564a1d 26 . . . . . . . . . 10 (¬ ((𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) → ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))) → (¬ ⊥ → 𝜑))
66 ax-1 6 . . . . . . . . . . . . . . 15 (¬ ((𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) → ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))) → (¬ ⊥ → ¬ ((𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) → ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓))))))))
6723a1d 26 . . . . . . . . . . . . . . 15 (¬ ((𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) → ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))) → (¬ ⊥ → (¬ ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓))))) ∨ ((𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) → ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))))))
6866, 67cnf2dd 39166 . . . . . . . . . . . . . 14 (¬ ((𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) → ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))) → (¬ ⊥ → ¬ ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))))
6926a1d 26 . . . . . . . . . . . . . 14 (¬ ((𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) → ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))) → (¬ ⊥ → (¬ (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))) ∨ ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓))))))))
7068, 69cnf2dd 39166 . . . . . . . . . . . . 13 (¬ ((𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) → ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))) → (¬ ⊥ → ¬ (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓))))))
7129a1d 26 . . . . . . . . . . . . 13 (¬ ((𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) → ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))) → (¬ ⊥ → (∃𝑦𝜑 ∨ (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))))
7270, 71cnf2dd 39166 . . . . . . . . . . . 12 (¬ ((𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) → ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))) → (¬ ⊥ → ∃𝑦𝜑))
7332a1d 26 . . . . . . . . . . . . 13 (¬ ((𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) → ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))) → (¬ ⊥ → ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) ∨ ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓))))))))
7468, 73cnf2dd 39166 . . . . . . . . . . . 12 (¬ ((𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) → ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))) → (¬ ⊥ → (∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑))))
7572, 74mpdd 44 . . . . . . . . . . 11 (¬ ((𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) → ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))) → (¬ ⊥ → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)))
76 tsbi3 39210 . . . . . . . . . . . 12 (¬ ((𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) → ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))) → ((𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ∨ ¬ 𝜑) ∨ ¬ (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)))
7776a1d 26 . . . . . . . . . . 11 (¬ ((𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) → ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))) → (¬ ⊥ → ((𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ∨ ¬ 𝜑) ∨ ¬ (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑))))
7875, 77cnfn2dd 39168 . . . . . . . . . 10 (¬ ((𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) → ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))) → (¬ ⊥ → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ∨ ¬ 𝜑)))
7965, 78cnfn2dd 39168 . . . . . . . . 9 (¬ ((𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) → ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))) → (¬ ⊥ → 𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V)))
8040a1d 26 . . . . . . . . . . . . . . . 16 (¬ ((𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) → ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))) → (¬ ⊥ → (¬ (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓))) ∨ (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))))
8170, 80cnf2dd 39166 . . . . . . . . . . . . . . 15 (¬ ((𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) → ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))) → (¬ ⊥ → ¬ (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))
8250a1d 26 . . . . . . . . . . . . . . 15 (¬ ((𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) → ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))) → (¬ ⊥ → (𝑦 = (𝑓‘𝑥) ∨ (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓))))))
8381, 82cnf2dd 39166 . . . . . . . . . . . . . 14 (¬ ((𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) → ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))) → (¬ ⊥ → 𝑦 = (𝑓‘𝑥)))
8483, 53syld 48 . . . . . . . . . . . . 13 (¬ ((𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) → ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))) → (¬ ⊥ → (𝜑 ↔ 𝜓)))
85 tsbi4 39211 . . . . . . . . . . . . . 14 (¬ ((𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) → ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))) → ((¬ 𝜑 ∨ 𝜓) ∨ ¬ (𝜑 ↔ 𝜓)))
8685a1d 26 . . . . . . . . . . . . 13 (¬ ((𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) → ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))) → (¬ ⊥ → ((¬ 𝜑 ∨ 𝜓) ∨ ¬ (𝜑 ↔ 𝜓))))
8784, 86cnfn2dd 39168 . . . . . . . . . . . 12 (¬ ((𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) → ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))) → (¬ ⊥ → (¬ 𝜑 ∨ 𝜓)))
8865, 87cnfn1dd 39167 . . . . . . . . . . 11 (¬ ((𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) → ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))) → (¬ ⊥ → 𝜓))
8988a1dd 51 . . . . . . . . . 10 (¬ ((𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) → ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))) → (¬ ⊥ → (∃𝑦𝜑 → 𝜓)))
90 tsbi1 39208 . . . . . . . . . . . 12 (¬ ((𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) → ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))) → ((¬ 𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ∨ ¬ (∃𝑦𝜑 → 𝜓)) ∨ (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓))))
9190a1d 26 . . . . . . . . . . 11 (¬ ((𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) → ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))) → (¬ ⊥ → ((¬ 𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ∨ ¬ (∃𝑦𝜑 → 𝜓)) ∨ (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))
9291or32dd 39169 . . . . . . . . . 10 (¬ ((𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) → ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))) → (¬ ⊥ → ((¬ 𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ∨ (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓))) ∨ ¬ (∃𝑦𝜑 → 𝜓))))
9389, 92cnfn2dd 39168 . . . . . . . . 9 (¬ ((𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) → ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))) → (¬ ⊥ → (¬ 𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ∨ (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))
9479, 93cnfn1dd 39167 . . . . . . . 8 (¬ ((𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) → ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))) → (¬ ⊥ → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓))))
9543a1d 26 . . . . . . . . 9 (¬ ((𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) → ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))) → (¬ ⊥ → (¬ (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)) ∨ (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓))))))
9681, 95cnf2dd 39166 . . . . . . . 8 (¬ ((𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) → ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))) → (¬ ⊥ → ¬ (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓))))
9794, 96contrd 39172 . . . . . . 7 (¬ ((𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) → ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))) → ⊥)
9897efald2 39155 . . . . . 6 ((𝑦 = (𝑓‘𝑥) → (𝜑 ↔ 𝜓)) → ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓))))))
9919, 98ax-mp 5 . . . . 5 ((∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝜑)) → (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))
1003, 99ax-mp 5 . . . 4 (∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓))))
1016a1i 11 . . . . . . 7 (¬ ∃𝑦𝜑 → 𝑦 ∈ V)
102 id 23 . . . . . . . . . . . 12 (¬ ((¬ ∃𝑦𝜑 → 𝑦 ∈ V) → ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝑦 ∈ V)) → (¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)))) → ¬ ((¬ ∃𝑦𝜑 → 𝑦 ∈ V) → ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝑦 ∈ V)) → (¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)))))
103 tsim2 39206 . . . . . . . . . . . . . . 15 (¬ ((¬ ∃𝑦𝜑 → 𝑦 ∈ V) → ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝑦 ∈ V)) → (¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)))) → (¬ ∃𝑦𝜑 ∨ (¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤))))
104103ord 878 . . . . . . . . . . . . . 14 (¬ ((¬ ∃𝑦𝜑 → 𝑦 ∈ V) → ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝑦 ∈ V)) → (¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)))) → (¬ ¬ ∃𝑦𝜑 → (¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤))))
105104a1dd 51 . . . . . . . . . . . . 13 (¬ ((¬ ∃𝑦𝜑 → 𝑦 ∈ V) → ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝑦 ∈ V)) → (¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)))) → (¬ ¬ ∃𝑦𝜑 → ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝑦 ∈ V)) → (¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)))))
106105a1dd 51 . . . . . . . . . . . 12 (¬ ((¬ ∃𝑦𝜑 → 𝑦 ∈ V) → ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝑦 ∈ V)) → (¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)))) → (¬ ¬ ∃𝑦𝜑 → ((¬ ∃𝑦𝜑 → 𝑦 ∈ V) → ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝑦 ∈ V)) → (¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤))))))
107102, 106mt3d 149 . . . . . . . . . . 11 (¬ ((¬ ∃𝑦𝜑 → 𝑦 ∈ V) → ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝑦 ∈ V)) → (¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)))) → ¬ ∃𝑦𝜑)
108107a1d 26 . . . . . . . . . 10 (¬ ((¬ ∃𝑦𝜑 → 𝑦 ∈ V) → ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝑦 ∈ V)) → (¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)))) → (¬ ⊥ → ¬ ∃𝑦𝜑))
109 simplim 168 . . . . . . . . . 10 (¬ ((¬ ∃𝑦𝜑 → 𝑦 ∈ V) → ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝑦 ∈ V)) → (¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)))) → (¬ ∃𝑦𝜑 → 𝑦 ∈ V))
110108, 109syld 48 . . . . . . . . 9 (¬ ((¬ ∃𝑦𝜑 → 𝑦 ∈ V) → ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝑦 ∈ V)) → (¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)))) → (¬ ⊥ → 𝑦 ∈ V))
111 tsim2 39206 . . . . . . . . . . . . . 14 (¬ ((¬ ∃𝑦𝜑 → 𝑦 ∈ V) → ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝑦 ∈ V)) → (¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)))) → ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝑦 ∈ V)) ∨ ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝑦 ∈ V)) → (¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)))))
112111ord 878 . . . . . . . . . . . . 13 (¬ ((¬ ∃𝑦𝜑 → 𝑦 ∈ V) → ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝑦 ∈ V)) → (¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)))) → (¬ (¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝑦 ∈ V)) → ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝑦 ∈ V)) → (¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)))))
113112a1dd 51 . . . . . . . . . . . 12 (¬ ((¬ ∃𝑦𝜑 → 𝑦 ∈ V) → ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝑦 ∈ V)) → (¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)))) → (¬ (¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝑦 ∈ V)) → ((¬ ∃𝑦𝜑 → 𝑦 ∈ V) → ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝑦 ∈ V)) → (¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤))))))
114102, 113mt3d 149 . . . . . . . . . . 11 (¬ ((¬ ∃𝑦𝜑 → 𝑦 ∈ V) → ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝑦 ∈ V)) → (¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)))) → (¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝑦 ∈ V)))
115108, 114syld 48 . . . . . . . . . 10 (¬ ((¬ ∃𝑦𝜑 → 𝑦 ∈ V) → ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝑦 ∈ V)) → (¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)))) → (¬ ⊥ → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝑦 ∈ V)))
116 id 23 . . . . . . . . . . . . . . . . . 18 (¬ (¬ (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝑦 ∈ V) ∨ ¬ 𝑦 ∈ V) → ¬ (¬ (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝑦 ∈ V) ∨ ¬ 𝑦 ∈ V))
117116notornotel2 39171 . . . . . . . . . . . . . . . . 17 (¬ (¬ (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝑦 ∈ V) ∨ ¬ 𝑦 ∈ V) → 𝑦 ∈ V)
118117a1i 11 . . . . . . . . . . . . . . . 16 (¬ ((¬ ∃𝑦𝜑 → 𝑦 ∈ V) → ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝑦 ∈ V)) → (¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)))) → (¬ (¬ (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝑦 ∈ V) ∨ ¬ 𝑦 ∈ V) → 𝑦 ∈ V))
119116notornotel1 39170 . . . . . . . . . . . . . . . . . 18 (¬ (¬ (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝑦 ∈ V) ∨ ¬ 𝑦 ∈ V) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝑦 ∈ V))
120119a1i 11 . . . . . . . . . . . . . . . . 17 (¬ ((¬ ∃𝑦𝜑 → 𝑦 ∈ V) → ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝑦 ∈ V)) → (¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)))) → (¬ (¬ (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝑦 ∈ V) ∨ ¬ 𝑦 ∈ V) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝑦 ∈ V)))
121 tsbi3 39210 . . . . . . . . . . . . . . . . . 18 (¬ ((¬ ∃𝑦𝜑 → 𝑦 ∈ V) → ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝑦 ∈ V)) → (¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)))) → ((𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ∨ ¬ 𝑦 ∈ V) ∨ ¬ (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝑦 ∈ V)))
122121a1d 26 . . . . . . . . . . . . . . . . 17 (¬ ((¬ ∃𝑦𝜑 → 𝑦 ∈ V) → ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝑦 ∈ V)) → (¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)))) → (¬ (¬ (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝑦 ∈ V) ∨ ¬ 𝑦 ∈ V) → ((𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ∨ ¬ 𝑦 ∈ V) ∨ ¬ (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝑦 ∈ V))))
123120, 122cnfn2dd 39168 . . . . . . . . . . . . . . . 16 (¬ ((¬ ∃𝑦𝜑 → 𝑦 ∈ V) → ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝑦 ∈ V)) → (¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)))) → (¬ (¬ (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝑦 ∈ V) ∨ ¬ 𝑦 ∈ V) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ∨ ¬ 𝑦 ∈ V)))
124118, 123cnfn2dd 39168 . . . . . . . . . . . . . . 15 (¬ ((¬ ∃𝑦𝜑 → 𝑦 ∈ V) → ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝑦 ∈ V)) → (¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)))) → (¬ (¬ (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝑦 ∈ V) ∨ ¬ 𝑦 ∈ V) → 𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V)))
125 trud 1579 . . . . . . . . . . . . . . . . 17 (¬ ((¬ ∃𝑦𝜑 → 𝑦 ∈ V) → ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝑦 ∈ V)) → (¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)))) → ⊤)
126125a1d 26 . . . . . . . . . . . . . . . 16 (¬ ((¬ ∃𝑦𝜑 → 𝑦 ∈ V) → ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝑦 ∈ V)) → (¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)))) → (¬ (¬ (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝑦 ∈ V) ∨ ¬ 𝑦 ∈ V) → ⊤))
127 tsbi1 39208 . . . . . . . . . . . . . . . . . 18 (¬ ((¬ ∃𝑦𝜑 → 𝑦 ∈ V) → ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝑦 ∈ V)) → (¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)))) → ((¬ 𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ∨ ¬ ⊤) ∨ (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)))
128127a1d 26 . . . . . . . . . . . . . . . . 17 (¬ ((¬ ∃𝑦𝜑 → 𝑦 ∈ V) → ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝑦 ∈ V)) → (¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)))) → (¬ (¬ (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝑦 ∈ V) ∨ ¬ 𝑦 ∈ V) → ((¬ 𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ∨ ¬ ⊤) ∨ (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤))))
129128or32dd 39169 . . . . . . . . . . . . . . . 16 (¬ ((¬ ∃𝑦𝜑 → 𝑦 ∈ V) → ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝑦 ∈ V)) → (¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)))) → (¬ (¬ (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝑦 ∈ V) ∨ ¬ 𝑦 ∈ V) → ((¬ 𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ∨ (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)) ∨ ¬ ⊤)))
130126, 129cnfn2dd 39168 . . . . . . . . . . . . . . 15 (¬ ((¬ ∃𝑦𝜑 → 𝑦 ∈ V) → ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝑦 ∈ V)) → (¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)))) → (¬ (¬ (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝑦 ∈ V) ∨ ¬ 𝑦 ∈ V) → (¬ 𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ∨ (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤))))
131124, 130cnfn1dd 39167 . . . . . . . . . . . . . 14 (¬ ((¬ ∃𝑦𝜑 → 𝑦 ∈ V) → ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝑦 ∈ V)) → (¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)))) → (¬ (¬ (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝑦 ∈ V) ∨ ¬ 𝑦 ∈ V) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)))
132131a1dd 51 . . . . . . . . . . . . 13 (¬ ((¬ ∃𝑦𝜑 → 𝑦 ∈ V) → ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝑦 ∈ V)) → (¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)))) → (¬ (¬ (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝑦 ∈ V) ∨ ¬ 𝑦 ∈ V) → (¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤))))
133132a1dd 51 . . . . . . . . . . . 12 (¬ ((¬ ∃𝑦𝜑 → 𝑦 ∈ V) → ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝑦 ∈ V)) → (¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)))) → (¬ (¬ (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝑦 ∈ V) ∨ ¬ 𝑦 ∈ V) → ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝑦 ∈ V)) → (¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)))))
134 ax-1 6 . . . . . . . . . . . . 13 (¬ ((¬ ∃𝑦𝜑 → 𝑦 ∈ V) → ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝑦 ∈ V)) → (¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)))) → (¬ (¬ (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝑦 ∈ V) ∨ ¬ 𝑦 ∈ V) → ¬ ((¬ ∃𝑦𝜑 → 𝑦 ∈ V) → ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝑦 ∈ V)) → (¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤))))))
135 tsim3 39207 . . . . . . . . . . . . . 14 (¬ ((¬ ∃𝑦𝜑 → 𝑦 ∈ V) → ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝑦 ∈ V)) → (¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)))) → (¬ ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝑦 ∈ V)) → (¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤))) ∨ ((¬ ∃𝑦𝜑 → 𝑦 ∈ V) → ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝑦 ∈ V)) → (¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤))))))
136135a1d 26 . . . . . . . . . . . . 13 (¬ ((¬ ∃𝑦𝜑 → 𝑦 ∈ V) → ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝑦 ∈ V)) → (¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)))) → (¬ (¬ (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝑦 ∈ V) ∨ ¬ 𝑦 ∈ V) → (¬ ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝑦 ∈ V)) → (¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤))) ∨ ((¬ ∃𝑦𝜑 → 𝑦 ∈ V) → ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝑦 ∈ V)) → (¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)))))))
137134, 136cnf2dd 39166 . . . . . . . . . . . 12 (¬ ((¬ ∃𝑦𝜑 → 𝑦 ∈ V) → ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝑦 ∈ V)) → (¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)))) → (¬ (¬ (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝑦 ∈ V) ∨ ¬ 𝑦 ∈ V) → ¬ ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝑦 ∈ V)) → (¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)))))
138133, 137contrd 39172 . . . . . . . . . . 11 (¬ ((¬ ∃𝑦𝜑 → 𝑦 ∈ V) → ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝑦 ∈ V)) → (¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)))) → (¬ (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝑦 ∈ V) ∨ ¬ 𝑦 ∈ V))
139138a1d 26 . . . . . . . . . 10 (¬ ((¬ ∃𝑦𝜑 → 𝑦 ∈ V) → ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝑦 ∈ V)) → (¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)))) → (¬ ⊥ → (¬ (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝑦 ∈ V) ∨ ¬ 𝑦 ∈ V)))
140115, 139cnfn1dd 39167 . . . . . . . . 9 (¬ ((¬ ∃𝑦𝜑 → 𝑦 ∈ V) → ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝑦 ∈ V)) → (¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)))) → (¬ ⊥ → ¬ 𝑦 ∈ V))
141110, 140contrd 39172 . . . . . . . 8 (¬ ((¬ ∃𝑦𝜑 → 𝑦 ∈ V) → ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝑦 ∈ V)) → (¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)))) → ⊥)
142141efald2 39155 . . . . . . 7 ((¬ ∃𝑦𝜑 → 𝑦 ∈ V) → ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝑦 ∈ V)) → (¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤))))
143101, 142ax-mp 5 . . . . . 6 ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ 𝑦 ∈ V)) → (¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)))
14410, 143ax-mp 5 . . . . 5 (¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤))
145 ax-1 6 . . . . . . . . . 10 (¬ ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)) → (¬ ∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓))))) → (¬ ⊥ → ¬ ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)) → (¬ ∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))))
146 tsim3 39207 . . . . . . . . . . 11 (¬ ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)) → (¬ ∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓))))) → (¬ (¬ ∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))) ∨ ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)) → (¬ ∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))))
147146a1d 26 . . . . . . . . . 10 (¬ ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)) → (¬ ∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓))))) → (¬ ⊥ → (¬ (¬ ∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))) ∨ ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)) → (¬ ∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓))))))))
148145, 147cnf2dd 39166 . . . . . . . . 9 (¬ ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)) → (¬ ∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓))))) → (¬ ⊥ → ¬ (¬ ∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓))))))
149 tsim2 39206 . . . . . . . . . 10 (¬ ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)) → (¬ ∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓))))) → (¬ ∃𝑦𝜑 ∨ (¬ ∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓))))))
150149a1d 26 . . . . . . . . 9 (¬ ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)) → (¬ ∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓))))) → (¬ ⊥ → (¬ ∃𝑦𝜑 ∨ (¬ ∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))))
151148, 150cnf2dd 39166 . . . . . . . 8 (¬ ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)) → (¬ ∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓))))) → (¬ ⊥ → ¬ ∃𝑦𝜑))
152 tsim2 39206 . . . . . . . . . 10 (¬ ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)) → (¬ ∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓))))) → ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)) ∨ ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)) → (¬ ∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))))
153152a1d 26 . . . . . . . . 9 (¬ ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)) → (¬ ∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓))))) → (¬ ⊥ → ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)) ∨ ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)) → (¬ ∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓))))))))
154145, 153cnf2dd 39166 . . . . . . . 8 (¬ ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)) → (¬ ∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓))))) → (¬ ⊥ → (¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤))))
155151, 154mpdd 44 . . . . . . 7 (¬ ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)) → (¬ ∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓))))) → (¬ ⊥ → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)))
156 id 23 . . . . . . . . . . 11 (¬ ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)) → (¬ ∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓))))) → ¬ ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)) → (¬ ∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓))))))
157 id 23 . . . . . . . . . . . . . . 15 (¬ (∃𝑦𝜑 → 𝜓) → ¬ (∃𝑦𝜑 → 𝜓))
158157a1i 11 . . . . . . . . . . . . . 14 (¬ ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)) → (¬ ∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓))))) → (¬ (∃𝑦𝜑 → 𝜓) → ¬ (∃𝑦𝜑 → 𝜓)))
159 tsim2 39206 . . . . . . . . . . . . . . 15 (¬ ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)) → (¬ ∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓))))) → (∃𝑦𝜑 ∨ (∃𝑦𝜑 → 𝜓)))
160159a1d 26 . . . . . . . . . . . . . 14 (¬ ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)) → (¬ ∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓))))) → (¬ (∃𝑦𝜑 → 𝜓) → (∃𝑦𝜑 ∨ (∃𝑦𝜑 → 𝜓))))
161158, 160cnf2dd 39166 . . . . . . . . . . . . 13 (¬ ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)) → (¬ ∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓))))) → (¬ (∃𝑦𝜑 → 𝜓) → ∃𝑦𝜑))
162149a1d 26 . . . . . . . . . . . . 13 (¬ ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)) → (¬ ∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓))))) → (¬ (∃𝑦𝜑 → 𝜓) → (¬ ∃𝑦𝜑 ∨ (¬ ∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))))
163161, 162cnfn1dd 39167 . . . . . . . . . . . 12 (¬ ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)) → (¬ ∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓))))) → (¬ (∃𝑦𝜑 → 𝜓) → (¬ ∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓))))))
164163a1dd 51 . . . . . . . . . . 11 (¬ ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)) → (¬ ∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓))))) → (¬ (∃𝑦𝜑 → 𝜓) → ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)) → (¬ ∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))))
165156, 164mt3d 149 . . . . . . . . . 10 (¬ ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)) → (¬ ∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓))))) → (∃𝑦𝜑 → 𝜓))
166165a1d 26 . . . . . . . . 9 (¬ ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)) → (¬ ∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓))))) → (¬ ⊥ → (∃𝑦𝜑 → 𝜓)))
167 tsim3 39207 . . . . . . . . . . . . 13 (¬ ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)) → (¬ ∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓))))) → (¬ (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓))) ∨ (¬ ∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓))))))
168167a1d 26 . . . . . . . . . . . 12 (¬ ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)) → (¬ ∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓))))) → (¬ ⊥ → (¬ (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓))) ∨ (¬ ∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))))
169148, 168cnf2dd 39166 . . . . . . . . . . 11 (¬ ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)) → (¬ ∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓))))) → (¬ ⊥ → ¬ (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))
170 tsim3 39207 . . . . . . . . . . . 12 (¬ ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)) → (¬ ∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓))))) → (¬ (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)) ∨ (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))
171170a1d 26 . . . . . . . . . . 11 (¬ ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)) → (¬ ∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓))))) → (¬ ⊥ → (¬ (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)) ∨ (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓))))))
172169, 171cnf2dd 39166 . . . . . . . . . 10 (¬ ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)) → (¬ ∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓))))) → (¬ ⊥ → ¬ (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓))))
173 tsbi1 39208 . . . . . . . . . . 11 (¬ ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)) → (¬ ∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓))))) → ((¬ 𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ∨ ¬ (∃𝑦𝜑 → 𝜓)) ∨ (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓))))
174173a1d 26 . . . . . . . . . 10 (¬ ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)) → (¬ ∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓))))) → (¬ ⊥ → ((¬ 𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ∨ ¬ (∃𝑦𝜑 → 𝜓)) ∨ (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))
175172, 174cnf2dd 39166 . . . . . . . . 9 (¬ ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)) → (¬ ∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓))))) → (¬ ⊥ → (¬ 𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ∨ ¬ (∃𝑦𝜑 → 𝜓))))
176166, 175cnfn2dd 39168 . . . . . . . 8 (¬ ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)) → (¬ ∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓))))) → (¬ ⊥ → ¬ 𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V)))
177 trud 1579 . . . . . . . . . 10 (¬ ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)) → (¬ ∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓))))) → ⊤)
178177a1d 26 . . . . . . . . 9 (¬ ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)) → (¬ ∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓))))) → (¬ ⊥ → ⊤))
179 tsbi3 39210 . . . . . . . . . . 11 (¬ ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)) → (¬ ∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓))))) → ((𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ∨ ¬ ⊤) ∨ ¬ (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)))
180179a1d 26 . . . . . . . . . 10 (¬ ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)) → (¬ ∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓))))) → (¬ ⊥ → ((𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ∨ ¬ ⊤) ∨ ¬ (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤))))
181180or32dd 39169 . . . . . . . . 9 (¬ ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)) → (¬ ∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓))))) → (¬ ⊥ → ((𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ∨ ¬ (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)) ∨ ¬ ⊤)))
182178, 181cnfn2dd 39168 . . . . . . . 8 (¬ ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)) → (¬ ∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓))))) → (¬ ⊥ → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ∨ ¬ (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤))))
183176, 182cnf1dd 39165 . . . . . . 7 (¬ ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)) → (¬ ∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓))))) → (¬ ⊥ → ¬ (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)))
184155, 183contrd 39172 . . . . . 6 (¬ ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)) → (¬ ∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓))))) → ⊥)
185184efald2 39155 . . . . 5 ((¬ ∃𝑦𝜑 → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ ⊤)) → (¬ ∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))))
186144, 185ax-mp 5 . . . 4 (¬ ∃𝑦𝜑 → (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓))))
187100, 186pm2.61i 184 . . 3 (𝑦 = (𝑓‘𝑥) → (𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) ↔ (∃𝑦𝜑 → 𝜓)))
18817, 18, 187ac6s3f 39246 . 2 (∀𝑥 ∈ 𝐴 ∃𝑦 𝑦 ∈ if(∃𝑦𝜑, {𝑦 ∣ 𝜑}, V) → ∃𝑓∀𝑥 ∈ 𝐴 (∃𝑦𝜑 → 𝜓))
18914, 188ax-mp 5 1 ∃𝑓∀𝑥 ∈ 𝐴 (∃𝑦𝜑 → 𝜓)
Colors of variables:    wff setvar class
This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∨ wo 861   = wceq 1569  ⊤wtru 1570  ⊥wfal 1581  ∃wex 1811  Ⅎwnf 1815   ∈ wcel 2146  {cab 2741  ∀wral 3080  Vcvv 3454  ifcif 4485  ‘cfv 6547
This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2196  ax-12 2215  ax-ext 2735  ax-rep 5235  ax-sep 5252  ax-nul 5263  ax-pow 5331  ax-pr 5395  ax-un 7761  ax-reg 9599  ax-inf2 9655  ax-ac2 10554
This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2101  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-int 4911  df-iun 4956  df-iin 4957  df-br 5107  df-opab 5171  df-mpt 5190  df-tr 5216  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-se 5609  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6311  df-ord 6372  df-on 6373  df-lim 6374  df-suc 6375  df-iota 6501  df-fun 6549  df-fn 6550  df-f 6551  df-f1 6552  df-fo 6553  df-f1o 6554  df-fv 6555  df-isom 6556  df-riota 7387  df-ov 7433  df-om 7888  df-2nd 8012  df-frecs 8313  df-wrecs 8344  df-recs 8393  df-rdg 8432  df-en 8988  df-r1 9781  df-rank 9782  df-scott 9942  df-card 10033  df-ac 10208
This theorem is used by:  ac6s6f  39248
  Copyright terms: Public domain W3C validator