Metamath Proof Explorer

Theorem axgroth4

Description: Alternate version of the Tarski-Grothendieck Axiom. ax-ac is used to derive this version. (Contributed by NM, 16-Apr-2007)

Ref Expression
Assertion axgroth4 ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ∃ 𝑣 ∈ 𝑦 ∀ 𝑤 ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ ( 𝑦 ∩ 𝑣 ) ) ∧ ∀ 𝑧 ( 𝑧 ⊆ 𝑦 → ( ( 𝑦 ∖ 𝑧 ) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦 ) ) )

Proof

Step Hyp Ref Expression
1 axgroth3 ⊢ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ 𝑦 ) ∧ ∃ 𝑤 ∈ 𝑦 ∀ 𝑢 ( 𝑢 ⊆ 𝑧 → 𝑢 ∈ 𝑤 ) ) ∧ ∀ 𝑧 ( 𝑧 ⊆ 𝑦 → ( ( 𝑦 ∖ 𝑧 ) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦 ) ) )
2 elequ2 ⊢ ( 𝑤 = 𝑣 → ( 𝑢 ∈ 𝑤 ↔ 𝑢 ∈ 𝑣 ) )
3 2 imbi2d ⊢ ( 𝑤 = 𝑣 → ( ( 𝑢 ⊆ 𝑧 → 𝑢 ∈ 𝑤 ) ↔ ( 𝑢 ⊆ 𝑧 → 𝑢 ∈ 𝑣 ) ) )
4 3 albidv ⊢ ( 𝑤 = 𝑣 → ( ∀ 𝑢 ( 𝑢 ⊆ 𝑧 → 𝑢 ∈ 𝑤 ) ↔ ∀ 𝑢 ( 𝑢 ⊆ 𝑧 → 𝑢 ∈ 𝑣 ) ) )
5 4 cbvrexvw ⊢ ( ∃ 𝑤 ∈ 𝑦 ∀ 𝑢 ( 𝑢 ⊆ 𝑧 → 𝑢 ∈ 𝑤 ) ↔ ∃ 𝑣 ∈ 𝑦 ∀ 𝑢 ( 𝑢 ⊆ 𝑧 → 𝑢 ∈ 𝑣 ) )
6 5 anbi2i ⊢ ( ( ∀ 𝑤 ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ 𝑦 ) ∧ ∃ 𝑤 ∈ 𝑦 ∀ 𝑢 ( 𝑢 ⊆ 𝑧 → 𝑢 ∈ 𝑤 ) ) ↔ ( ∀ 𝑤 ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ 𝑦 ) ∧ ∃ 𝑣 ∈ 𝑦 ∀ 𝑢 ( 𝑢 ⊆ 𝑧 → 𝑢 ∈ 𝑣 ) ) )
7 r19.42v ⊢ ( ∃ 𝑣 ∈ 𝑦 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ 𝑦 ) ∧ ∀ 𝑢 ( 𝑢 ⊆ 𝑧 → 𝑢 ∈ 𝑣 ) ) ↔ ( ∀ 𝑤 ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ 𝑦 ) ∧ ∃ 𝑣 ∈ 𝑦 ∀ 𝑢 ( 𝑢 ⊆ 𝑧 → 𝑢 ∈ 𝑣 ) ) )
8 sseq1 ⊢ ( 𝑢 = 𝑤 → ( 𝑢 ⊆ 𝑧 ↔ 𝑤 ⊆ 𝑧 ) )
9 elequ1 ⊢ ( 𝑢 = 𝑤 → ( 𝑢 ∈ 𝑣 ↔ 𝑤 ∈ 𝑣 ) )
10 8 9 imbi12d ⊢ ( 𝑢 = 𝑤 → ( ( 𝑢 ⊆ 𝑧 → 𝑢 ∈ 𝑣 ) ↔ ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ 𝑣 ) ) )
11 10 cbvalvw ⊢ ( ∀ 𝑢 ( 𝑢 ⊆ 𝑧 → 𝑢 ∈ 𝑣 ) ↔ ∀ 𝑤 ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ 𝑣 ) )
12 11 anbi2i ⊢ ( ( ∀ 𝑤 ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ 𝑦 ) ∧ ∀ 𝑢 ( 𝑢 ⊆ 𝑧 → 𝑢 ∈ 𝑣 ) ) ↔ ( ∀ 𝑤 ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ 𝑦 ) ∧ ∀ 𝑤 ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ 𝑣 ) ) )
13 19.26 ⊢ ( ∀ 𝑤 ( ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ 𝑦 ) ∧ ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ 𝑣 ) ) ↔ ( ∀ 𝑤 ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ 𝑦 ) ∧ ∀ 𝑤 ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ 𝑣 ) ) )
14 pm4.76 ⊢ ( ( ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ 𝑦 ) ∧ ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ 𝑣 ) ) ↔ ( 𝑤 ⊆ 𝑧 → ( 𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣 ) ) )
15 elin ⊢ ( 𝑤 ∈ ( 𝑦 ∩ 𝑣 ) ↔ ( 𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣 ) )
16 15 imbi2i ⊢ ( ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ ( 𝑦 ∩ 𝑣 ) ) ↔ ( 𝑤 ⊆ 𝑧 → ( 𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑣 ) ) )
17 14 16 bitr4i ⊢ ( ( ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ 𝑦 ) ∧ ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ 𝑣 ) ) ↔ ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ ( 𝑦 ∩ 𝑣 ) ) )
18 17 albii ⊢ ( ∀ 𝑤 ( ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ 𝑦 ) ∧ ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ 𝑣 ) ) ↔ ∀ 𝑤 ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ ( 𝑦 ∩ 𝑣 ) ) )
19 12 13 18 3bitr2i ⊢ ( ( ∀ 𝑤 ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ 𝑦 ) ∧ ∀ 𝑢 ( 𝑢 ⊆ 𝑧 → 𝑢 ∈ 𝑣 ) ) ↔ ∀ 𝑤 ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ ( 𝑦 ∩ 𝑣 ) ) )
20 19 rexbii ⊢ ( ∃ 𝑣 ∈ 𝑦 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ 𝑦 ) ∧ ∀ 𝑢 ( 𝑢 ⊆ 𝑧 → 𝑢 ∈ 𝑣 ) ) ↔ ∃ 𝑣 ∈ 𝑦 ∀ 𝑤 ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ ( 𝑦 ∩ 𝑣 ) ) )
21 6 7 20 3bitr2i ⊢ ( ( ∀ 𝑤 ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ 𝑦 ) ∧ ∃ 𝑤 ∈ 𝑦 ∀ 𝑢 ( 𝑢 ⊆ 𝑧 → 𝑢 ∈ 𝑤 ) ) ↔ ∃ 𝑣 ∈ 𝑦 ∀ 𝑤 ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ ( 𝑦 ∩ 𝑣 ) ) )
22 21 ralbii ⊢ ( ∀ 𝑧 ∈ 𝑦 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ 𝑦 ) ∧ ∃ 𝑤 ∈ 𝑦 ∀ 𝑢 ( 𝑢 ⊆ 𝑧 → 𝑢 ∈ 𝑤 ) ) ↔ ∀ 𝑧 ∈ 𝑦 ∃ 𝑣 ∈ 𝑦 ∀ 𝑤 ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ ( 𝑦 ∩ 𝑣 ) ) )
23 22 3anbi2i ⊢ ( ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ 𝑦 ) ∧ ∃ 𝑤 ∈ 𝑦 ∀ 𝑢 ( 𝑢 ⊆ 𝑧 → 𝑢 ∈ 𝑤 ) ) ∧ ∀ 𝑧 ( 𝑧 ⊆ 𝑦 → ( ( 𝑦 ∖ 𝑧 ) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦 ) ) ) ↔ ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ∃ 𝑣 ∈ 𝑦 ∀ 𝑤 ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ ( 𝑦 ∩ 𝑣 ) ) ∧ ∀ 𝑧 ( 𝑧 ⊆ 𝑦 → ( ( 𝑦 ∖ 𝑧 ) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦 ) ) ) )
24 23 exbii ⊢ ( ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ( ∀ 𝑤 ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ 𝑦 ) ∧ ∃ 𝑤 ∈ 𝑦 ∀ 𝑢 ( 𝑢 ⊆ 𝑧 → 𝑢 ∈ 𝑤 ) ) ∧ ∀ 𝑧 ( 𝑧 ⊆ 𝑦 → ( ( 𝑦 ∖ 𝑧 ) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦 ) ) ) ↔ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ∃ 𝑣 ∈ 𝑦 ∀ 𝑤 ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ ( 𝑦 ∩ 𝑣 ) ) ∧ ∀ 𝑧 ( 𝑧 ⊆ 𝑦 → ( ( 𝑦 ∖ 𝑧 ) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦 ) ) ) )
25 1 24 mpbi ⊢ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ∃ 𝑣 ∈ 𝑦 ∀ 𝑤 ( 𝑤 ⊆ 𝑧 → 𝑤 ∈ ( 𝑦 ∩ 𝑣 ) ) ∧ ∀ 𝑧 ( 𝑧 ⊆ 𝑦 → ( ( 𝑦 ∖ 𝑧 ) ≼ 𝑧 ∨ 𝑧 ∈ 𝑦 ) ) )