Metamath Proof Explorer


Theorem axinfprim

Description: ax-inf without distinct variable conditions or defined symbols. (New usage is discouraged.) (Contributed by Scott Fenton, 13-Oct-2010)

Ref Expression
Assertion axinfprim ¬ ∀ 𝑥 ¬ ( 𝑦𝑧 → ¬ ( 𝑦𝑥 → ¬ ∀ 𝑦 ( 𝑦𝑥 → ¬ ∀ 𝑧 ( 𝑦𝑧 → ¬ 𝑧𝑥 ) ) ) )

Proof

Step Hyp Ref Expression
1 axinfnd 𝑥 ( 𝑦𝑧 → ( 𝑦𝑥 ∧ ∀ 𝑦 ( 𝑦𝑥 → ∃ 𝑧 ( 𝑦𝑧𝑧𝑥 ) ) ) )
2 df-an ( ( 𝑦𝑧𝑧𝑥 ) ↔ ¬ ( 𝑦𝑧 → ¬ 𝑧𝑥 ) )
3 2 exbii ( ∃ 𝑧 ( 𝑦𝑧𝑧𝑥 ) ↔ ∃ 𝑧 ¬ ( 𝑦𝑧 → ¬ 𝑧𝑥 ) )
4 exnal ( ∃ 𝑧 ¬ ( 𝑦𝑧 → ¬ 𝑧𝑥 ) ↔ ¬ ∀ 𝑧 ( 𝑦𝑧 → ¬ 𝑧𝑥 ) )
5 3 4 bitri ( ∃ 𝑧 ( 𝑦𝑧𝑧𝑥 ) ↔ ¬ ∀ 𝑧 ( 𝑦𝑧 → ¬ 𝑧𝑥 ) )
6 5 imbi2i ( ( 𝑦𝑥 → ∃ 𝑧 ( 𝑦𝑧𝑧𝑥 ) ) ↔ ( 𝑦𝑥 → ¬ ∀ 𝑧 ( 𝑦𝑧 → ¬ 𝑧𝑥 ) ) )
7 6 albii ( ∀ 𝑦 ( 𝑦𝑥 → ∃ 𝑧 ( 𝑦𝑧𝑧𝑥 ) ) ↔ ∀ 𝑦 ( 𝑦𝑥 → ¬ ∀ 𝑧 ( 𝑦𝑧 → ¬ 𝑧𝑥 ) ) )
8 7 anbi2i ( ( 𝑦𝑥 ∧ ∀ 𝑦 ( 𝑦𝑥 → ∃ 𝑧 ( 𝑦𝑧𝑧𝑥 ) ) ) ↔ ( 𝑦𝑥 ∧ ∀ 𝑦 ( 𝑦𝑥 → ¬ ∀ 𝑧 ( 𝑦𝑧 → ¬ 𝑧𝑥 ) ) ) )
9 df-an ( ( 𝑦𝑥 ∧ ∀ 𝑦 ( 𝑦𝑥 → ¬ ∀ 𝑧 ( 𝑦𝑧 → ¬ 𝑧𝑥 ) ) ) ↔ ¬ ( 𝑦𝑥 → ¬ ∀ 𝑦 ( 𝑦𝑥 → ¬ ∀ 𝑧 ( 𝑦𝑧 → ¬ 𝑧𝑥 ) ) ) )
10 8 9 bitri ( ( 𝑦𝑥 ∧ ∀ 𝑦 ( 𝑦𝑥 → ∃ 𝑧 ( 𝑦𝑧𝑧𝑥 ) ) ) ↔ ¬ ( 𝑦𝑥 → ¬ ∀ 𝑦 ( 𝑦𝑥 → ¬ ∀ 𝑧 ( 𝑦𝑧 → ¬ 𝑧𝑥 ) ) ) )
11 10 imbi2i ( ( 𝑦𝑧 → ( 𝑦𝑥 ∧ ∀ 𝑦 ( 𝑦𝑥 → ∃ 𝑧 ( 𝑦𝑧𝑧𝑥 ) ) ) ) ↔ ( 𝑦𝑧 → ¬ ( 𝑦𝑥 → ¬ ∀ 𝑦 ( 𝑦𝑥 → ¬ ∀ 𝑧 ( 𝑦𝑧 → ¬ 𝑧𝑥 ) ) ) ) )
12 11 exbii ( ∃ 𝑥 ( 𝑦𝑧 → ( 𝑦𝑥 ∧ ∀ 𝑦 ( 𝑦𝑥 → ∃ 𝑧 ( 𝑦𝑧𝑧𝑥 ) ) ) ) ↔ ∃ 𝑥 ( 𝑦𝑧 → ¬ ( 𝑦𝑥 → ¬ ∀ 𝑦 ( 𝑦𝑥 → ¬ ∀ 𝑧 ( 𝑦𝑧 → ¬ 𝑧𝑥 ) ) ) ) )
13 df-ex ( ∃ 𝑥 ( 𝑦𝑧 → ¬ ( 𝑦𝑥 → ¬ ∀ 𝑦 ( 𝑦𝑥 → ¬ ∀ 𝑧 ( 𝑦𝑧 → ¬ 𝑧𝑥 ) ) ) ) ↔ ¬ ∀ 𝑥 ¬ ( 𝑦𝑧 → ¬ ( 𝑦𝑥 → ¬ ∀ 𝑦 ( 𝑦𝑥 → ¬ ∀ 𝑧 ( 𝑦𝑧 → ¬ 𝑧𝑥 ) ) ) ) )
14 12 13 bitri ( ∃ 𝑥 ( 𝑦𝑧 → ( 𝑦𝑥 ∧ ∀ 𝑦 ( 𝑦𝑥 → ∃ 𝑧 ( 𝑦𝑧𝑧𝑥 ) ) ) ) ↔ ¬ ∀ 𝑥 ¬ ( 𝑦𝑧 → ¬ ( 𝑦𝑥 → ¬ ∀ 𝑦 ( 𝑦𝑥 → ¬ ∀ 𝑧 ( 𝑦𝑧 → ¬ 𝑧𝑥 ) ) ) ) )
15 1 14 mpbi ¬ ∀ 𝑥 ¬ ( 𝑦𝑧 → ¬ ( 𝑦𝑥 → ¬ ∀ 𝑦 ( 𝑦𝑥 → ¬ ∀ 𝑧 ( 𝑦𝑧 → ¬ 𝑧𝑥 ) ) ) )