Metamath Proof Explorer

Theorem kmlem1

Description: Lemma for 5-quantifier AC of Kurt Maes, Th. 4, 1 => 2. (Contributed by NM, 5-Apr-2004)

Ref Expression
Assertion kmlem1 ⊢∀x∀z∈xz≠∅∧∀z∈x∀w∈xφ→∃y∀z∈xψ→∀x∀z∈x∀w∈xφ→∃y∀z∈xz≠∅→ψ

Proof

Step Hyp Ref Expression
1 vex ⊢v∈V
2 1 rabex ⊢u∈v|u≠∅∈V
3 raleq ⊢x=u∈v|u≠∅→∀z∈xz≠∅↔∀z∈u∈v|u≠∅z≠∅
4 raleq ⊢x=u∈v|u≠∅→∀w∈xφ↔∀w∈u∈v|u≠∅φ
5 4 raleqbi1dv ⊢x=u∈v|u≠∅→∀z∈x∀w∈xφ↔∀z∈u∈v|u≠∅∀w∈u∈v|u≠∅φ
6 3 5 anbi12d ⊢x=u∈v|u≠∅→∀z∈xz≠∅∧∀z∈x∀w∈xφ↔∀z∈u∈v|u≠∅z≠∅∧∀z∈u∈v|u≠∅∀w∈u∈v|u≠∅φ
7 raleq ⊢x=u∈v|u≠∅→∀z∈xψ↔∀z∈u∈v|u≠∅ψ
8 7 exbidv ⊢x=u∈v|u≠∅→∃y∀z∈xψ↔∃y∀z∈u∈v|u≠∅ψ
9 6 8 imbi12d ⊢x=u∈v|u≠∅→∀z∈xz≠∅∧∀z∈x∀w∈xφ→∃y∀z∈xψ↔∀z∈u∈v|u≠∅z≠∅∧∀z∈u∈v|u≠∅∀w∈u∈v|u≠∅φ→∃y∀z∈u∈v|u≠∅ψ
10 2 9 spcv ⊢∀x∀z∈xz≠∅∧∀z∈x∀w∈xφ→∃y∀z∈xψ→∀z∈u∈v|u≠∅z≠∅∧∀z∈u∈v|u≠∅∀w∈u∈v|u≠∅φ→∃y∀z∈u∈v|u≠∅ψ
11 10 alrimiv ⊢∀x∀z∈xz≠∅∧∀z∈x∀w∈xφ→∃y∀z∈xψ→∀v∀z∈u∈v|u≠∅z≠∅∧∀z∈u∈v|u≠∅∀w∈u∈v|u≠∅φ→∃y∀z∈u∈v|u≠∅ψ
12 elrabi ⊢z∈u∈v|u≠∅→z∈v
13 elrabi ⊢w∈u∈v|u≠∅→w∈v
14 13 imim1i ⊢w∈v→φ→w∈u∈v|u≠∅→φ
15 14 ralimi2 ⊢∀w∈vφ→∀w∈u∈v|u≠∅φ
16 12 15 imim12i ⊢z∈v→∀w∈vφ→z∈u∈v|u≠∅→∀w∈u∈v|u≠∅φ
17 16 ralimi2 ⊢∀z∈v∀w∈vφ→∀z∈u∈v|u≠∅∀w∈u∈v|u≠∅φ
18 neeq1 ⊢u=z→u≠∅↔z≠∅
19 18 elrab ⊢z∈u∈v|u≠∅↔z∈v∧z≠∅
20 19 simprbi ⊢z∈u∈v|u≠∅→z≠∅
21 20 rgen ⊢∀z∈u∈v|u≠∅z≠∅
22 17 21 jctil ⊢∀z∈v∀w∈vφ→∀z∈u∈v|u≠∅z≠∅∧∀z∈u∈v|u≠∅∀w∈u∈v|u≠∅φ
23 19 biimpri ⊢z∈v∧z≠∅→z∈u∈v|u≠∅
24 23 imim1i ⊢z∈u∈v|u≠∅→ψ→z∈v∧z≠∅→ψ
25 24 expd ⊢z∈u∈v|u≠∅→ψ→z∈v→z≠∅→ψ
26 25 ralimi2 ⊢∀z∈u∈v|u≠∅ψ→∀z∈vz≠∅→ψ
27 26 eximi ⊢∃y∀z∈u∈v|u≠∅ψ→∃y∀z∈vz≠∅→ψ
28 22 27 imim12i ⊢∀z∈u∈v|u≠∅z≠∅∧∀z∈u∈v|u≠∅∀w∈u∈v|u≠∅φ→∃y∀z∈u∈v|u≠∅ψ→∀z∈v∀w∈vφ→∃y∀z∈vz≠∅→ψ
29 11 28 sylg ⊢∀x∀z∈xz≠∅∧∀z∈x∀w∈xφ→∃y∀z∈xψ→∀v∀z∈v∀w∈vφ→∃y∀z∈vz≠∅→ψ
30 raleq ⊢v=x→∀w∈vφ↔∀w∈xφ
31 30 raleqbi1dv ⊢v=x→∀z∈v∀w∈vφ↔∀z∈x∀w∈xφ
32 raleq ⊢v=x→∀z∈vz≠∅→ψ↔∀z∈xz≠∅→ψ
33 32 exbidv ⊢v=x→∃y∀z∈vz≠∅→ψ↔∃y∀z∈xz≠∅→ψ
34 31 33 imbi12d ⊢v=x→∀z∈v∀w∈vφ→∃y∀z∈vz≠∅→ψ↔∀z∈x∀w∈xφ→∃y∀z∈xz≠∅→ψ
35 34 cbvalvw ⊢∀v∀z∈v∀w∈vφ→∃y∀z∈vz≠∅→ψ↔∀x∀z∈x∀w∈xφ→∃y∀z∈xz≠∅→ψ
36 29 35 sylib ⊢∀x∀z∈xz≠∅∧∀z∈x∀w∈xφ→∃y∀z∈xψ→∀x∀z∈x∀w∈xφ→∃y∀z∈xz≠∅→ψ