Metamath Proof Explorer

Theorem sswfaxreg

Description: A subclass of the class of well-founded sets models the Axiom of Regularity ax-reg . Lemma II.2.4(2) of Kunen2 p. 111. (Contributed by Eric Schmidt, 19-Oct-2025)

Ref Expression
Assertion sswfaxreg ( 𝑀 ⊆ ∪ ( 𝑅1 “ On ) → ∀ 𝑥 ∈ 𝑀 ( ∃ 𝑦 ∈ 𝑀 𝑦 ∈ 𝑥 → ∃ 𝑦 ∈ 𝑀 ( 𝑦 ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝑀 ( 𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑥 ) ) ) )

Proof

Step Hyp Ref Expression
1 inn0 ⊢ ( ( 𝑀 ∩ 𝑥 ) ≠ ∅ ↔ ∃ 𝑦 ∈ 𝑀 𝑦 ∈ 𝑥 )
2 ssinss1 ⊢ ( 𝑀 ⊆ ∪ ( 𝑅1 “ On ) → ( 𝑀 ∩ 𝑥 ) ⊆ ∪ ( 𝑅1 “ On ) )
3 vex ⊢ 𝑥 ∈ V
4 3 inex2 ⊢ ( 𝑀 ∩ 𝑥 ) ∈ V
5 wffr ⊢ E Fr ∪ ( 𝑅1 “ On )
6 fri ⊢ ( ( ( ( 𝑀 ∩ 𝑥 ) ∈ V ∧ E Fr ∪ ( 𝑅1 “ On ) ) ∧ ( ( 𝑀 ∩ 𝑥 ) ⊆ ∪ ( 𝑅1 “ On ) ∧ ( 𝑀 ∩ 𝑥 ) ≠ ∅ ) ) → ∃ 𝑦 ∈ ( 𝑀 ∩ 𝑥 ) ∀ 𝑧 ∈ ( 𝑀 ∩ 𝑥 ) ¬ 𝑧 E 𝑦 )
7 4 5 6 mpanl12 ⊢ ( ( ( 𝑀 ∩ 𝑥 ) ⊆ ∪ ( 𝑅1 “ On ) ∧ ( 𝑀 ∩ 𝑥 ) ≠ ∅ ) → ∃ 𝑦 ∈ ( 𝑀 ∩ 𝑥 ) ∀ 𝑧 ∈ ( 𝑀 ∩ 𝑥 ) ¬ 𝑧 E 𝑦 )
8 2 7 sylan ⊢ ( ( 𝑀 ⊆ ∪ ( 𝑅1 “ On ) ∧ ( 𝑀 ∩ 𝑥 ) ≠ ∅ ) → ∃ 𝑦 ∈ ( 𝑀 ∩ 𝑥 ) ∀ 𝑧 ∈ ( 𝑀 ∩ 𝑥 ) ¬ 𝑧 E 𝑦 )
9 ralin ⊢ ( ∀ 𝑧 ∈ ( 𝑀 ∩ 𝑥 ) ¬ 𝑧 E 𝑦 ↔ ∀ 𝑧 ∈ 𝑀 ( 𝑧 ∈ 𝑥 → ¬ 𝑧 E 𝑦 ) )
10 con2b ⊢ ( ( 𝑧 ∈ 𝑥 → ¬ 𝑧 E 𝑦 ) ↔ ( 𝑧 E 𝑦 → ¬ 𝑧 ∈ 𝑥 ) )
11 epel ⊢ ( 𝑧 E 𝑦 ↔ 𝑧 ∈ 𝑦 )
12 11 imbi1i ⊢ ( ( 𝑧 E 𝑦 → ¬ 𝑧 ∈ 𝑥 ) ↔ ( 𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑥 ) )
13 10 12 bitri ⊢ ( ( 𝑧 ∈ 𝑥 → ¬ 𝑧 E 𝑦 ) ↔ ( 𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑥 ) )
14 13 ralbii ⊢ ( ∀ 𝑧 ∈ 𝑀 ( 𝑧 ∈ 𝑥 → ¬ 𝑧 E 𝑦 ) ↔ ∀ 𝑧 ∈ 𝑀 ( 𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑥 ) )
15 9 14 bitri ⊢ ( ∀ 𝑧 ∈ ( 𝑀 ∩ 𝑥 ) ¬ 𝑧 E 𝑦 ↔ ∀ 𝑧 ∈ 𝑀 ( 𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑥 ) )
16 15 rexbii ⊢ ( ∃ 𝑦 ∈ ( 𝑀 ∩ 𝑥 ) ∀ 𝑧 ∈ ( 𝑀 ∩ 𝑥 ) ¬ 𝑧 E 𝑦 ↔ ∃ 𝑦 ∈ ( 𝑀 ∩ 𝑥 ) ∀ 𝑧 ∈ 𝑀 ( 𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑥 ) )
17 rexin ⊢ ( ∃ 𝑦 ∈ ( 𝑀 ∩ 𝑥 ) ∀ 𝑧 ∈ 𝑀 ( 𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑥 ) ↔ ∃ 𝑦 ∈ 𝑀 ( 𝑦 ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝑀 ( 𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑥 ) ) )
18 16 17 bitri ⊢ ( ∃ 𝑦 ∈ ( 𝑀 ∩ 𝑥 ) ∀ 𝑧 ∈ ( 𝑀 ∩ 𝑥 ) ¬ 𝑧 E 𝑦 ↔ ∃ 𝑦 ∈ 𝑀 ( 𝑦 ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝑀 ( 𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑥 ) ) )
19 8 18 sylib ⊢ ( ( 𝑀 ⊆ ∪ ( 𝑅1 “ On ) ∧ ( 𝑀 ∩ 𝑥 ) ≠ ∅ ) → ∃ 𝑦 ∈ 𝑀 ( 𝑦 ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝑀 ( 𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑥 ) ) )
20 1 19 sylan2br ⊢ ( ( 𝑀 ⊆ ∪ ( 𝑅1 “ On ) ∧ ∃ 𝑦 ∈ 𝑀 𝑦 ∈ 𝑥 ) → ∃ 𝑦 ∈ 𝑀 ( 𝑦 ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝑀 ( 𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑥 ) ) )
21 20 ex ⊢ ( 𝑀 ⊆ ∪ ( 𝑅1 “ On ) → ( ∃ 𝑦 ∈ 𝑀 𝑦 ∈ 𝑥 → ∃ 𝑦 ∈ 𝑀 ( 𝑦 ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝑀 ( 𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑥 ) ) ) )
22 21 ralrimivw ⊢ ( 𝑀 ⊆ ∪ ( 𝑅1 “ On ) → ∀ 𝑥 ∈ 𝑀 ( ∃ 𝑦 ∈ 𝑀 𝑦 ∈ 𝑥 → ∃ 𝑦 ∈ 𝑀 ( 𝑦 ∈ 𝑥 ∧ ∀ 𝑧 ∈ 𝑀 ( 𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑥 ) ) ) )