Metamath Proof Explorer

Theorem dfon2lem9

Description: Lemma for dfon2 . A class of new ordinals is well-founded by _E . (Contributed by Scott Fenton, 3-Mar-2011)

Ref Expression
Assertion dfon2lem9 ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑥 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑥 ) → E Fr 𝐴 )

Proof

Step Hyp Ref Expression
1 ssralv ⊢ ( 𝑧 ⊆ 𝐴 → ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑥 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑥 ) → ∀ 𝑥 ∈ 𝑧 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑥 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑥 ) ) )
2 dfon2lem8 ⊢ ( ( 𝑧 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑧 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑥 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑥 ) ) → ( ∀ 𝑢 ( ( 𝑢 ⊊ ∩ 𝑧 ∧ Tr 𝑢 ) → 𝑢 ∈ ∩ 𝑧 ) ∧ ∩ 𝑧 ∈ 𝑧 ) )
3 2 simprd ⊢ ( ( 𝑧 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑧 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑥 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑥 ) ) → ∩ 𝑧 ∈ 𝑧 )
4 intss1 ⊢ ( 𝑡 ∈ 𝑧 → ∩ 𝑧 ⊆ 𝑡 )
5 2 simpld ⊢ ( ( 𝑧 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑧 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑥 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑥 ) ) → ∀ 𝑢 ( ( 𝑢 ⊊ ∩ 𝑧 ∧ Tr 𝑢 ) → 𝑢 ∈ ∩ 𝑧 ) )
6 intex ⊢ ( 𝑧 ≠ ∅ ↔ ∩ 𝑧 ∈ V )
7 dfon2lem3 ⊢ ( ∩ 𝑧 ∈ V → ( ∀ 𝑢 ( ( 𝑢 ⊊ ∩ 𝑧 ∧ Tr 𝑢 ) → 𝑢 ∈ ∩ 𝑧 ) → ( Tr ∩ 𝑧 ∧ ∀ 𝑥 ∈ ∩ 𝑧 ¬ 𝑥 ∈ 𝑥 ) ) )
8 7 imp ⊢ ( ( ∩ 𝑧 ∈ V ∧ ∀ 𝑢 ( ( 𝑢 ⊊ ∩ 𝑧 ∧ Tr 𝑢 ) → 𝑢 ∈ ∩ 𝑧 ) ) → ( Tr ∩ 𝑧 ∧ ∀ 𝑥 ∈ ∩ 𝑧 ¬ 𝑥 ∈ 𝑥 ) )
9 8 simprd ⊢ ( ( ∩ 𝑧 ∈ V ∧ ∀ 𝑢 ( ( 𝑢 ⊊ ∩ 𝑧 ∧ Tr 𝑢 ) → 𝑢 ∈ ∩ 𝑧 ) ) → ∀ 𝑥 ∈ ∩ 𝑧 ¬ 𝑥 ∈ 𝑥 )
10 untelirr ⊢ ( ∀ 𝑥 ∈ ∩ 𝑧 ¬ 𝑥 ∈ 𝑥 → ¬ ∩ 𝑧 ∈ ∩ 𝑧 )
11 9 10 syl ⊢ ( ( ∩ 𝑧 ∈ V ∧ ∀ 𝑢 ( ( 𝑢 ⊊ ∩ 𝑧 ∧ Tr 𝑢 ) → 𝑢 ∈ ∩ 𝑧 ) ) → ¬ ∩ 𝑧 ∈ ∩ 𝑧 )
12 eleq1 ⊢ ( ∩ 𝑧 = 𝑡 → ( ∩ 𝑧 ∈ ∩ 𝑧 ↔ 𝑡 ∈ ∩ 𝑧 ) )
13 12 notbid ⊢ ( ∩ 𝑧 = 𝑡 → ( ¬ ∩ 𝑧 ∈ ∩ 𝑧 ↔ ¬ 𝑡 ∈ ∩ 𝑧 ) )
14 11 13 syl5ibcom ⊢ ( ( ∩ 𝑧 ∈ V ∧ ∀ 𝑢 ( ( 𝑢 ⊊ ∩ 𝑧 ∧ Tr 𝑢 ) → 𝑢 ∈ ∩ 𝑧 ) ) → ( ∩ 𝑧 = 𝑡 → ¬ 𝑡 ∈ ∩ 𝑧 ) )
15 14 a1dd ⊢ ( ( ∩ 𝑧 ∈ V ∧ ∀ 𝑢 ( ( 𝑢 ⊊ ∩ 𝑧 ∧ Tr 𝑢 ) → 𝑢 ∈ ∩ 𝑧 ) ) → ( ∩ 𝑧 = 𝑡 → ( ∩ 𝑧 ⊆ 𝑡 → ¬ 𝑡 ∈ ∩ 𝑧 ) ) )
16 8 simpld ⊢ ( ( ∩ 𝑧 ∈ V ∧ ∀ 𝑢 ( ( 𝑢 ⊊ ∩ 𝑧 ∧ Tr 𝑢 ) → 𝑢 ∈ ∩ 𝑧 ) ) → Tr ∩ 𝑧 )
17 trss ⊢ ( Tr ∩ 𝑧 → ( 𝑡 ∈ ∩ 𝑧 → 𝑡 ⊆ ∩ 𝑧 ) )
18 16 17 syl ⊢ ( ( ∩ 𝑧 ∈ V ∧ ∀ 𝑢 ( ( 𝑢 ⊊ ∩ 𝑧 ∧ Tr 𝑢 ) → 𝑢 ∈ ∩ 𝑧 ) ) → ( 𝑡 ∈ ∩ 𝑧 → 𝑡 ⊆ ∩ 𝑧 ) )
19 eqss ⊢ ( ∩ 𝑧 = 𝑡 ↔ ( ∩ 𝑧 ⊆ 𝑡 ∧ 𝑡 ⊆ ∩ 𝑧 ) )
20 19 simplbi2com ⊢ ( 𝑡 ⊆ ∩ 𝑧 → ( ∩ 𝑧 ⊆ 𝑡 → ∩ 𝑧 = 𝑡 ) )
21 18 20 syl6 ⊢ ( ( ∩ 𝑧 ∈ V ∧ ∀ 𝑢 ( ( 𝑢 ⊊ ∩ 𝑧 ∧ Tr 𝑢 ) → 𝑢 ∈ ∩ 𝑧 ) ) → ( 𝑡 ∈ ∩ 𝑧 → ( ∩ 𝑧 ⊆ 𝑡 → ∩ 𝑧 = 𝑡 ) ) )
22 21 com23 ⊢ ( ( ∩ 𝑧 ∈ V ∧ ∀ 𝑢 ( ( 𝑢 ⊊ ∩ 𝑧 ∧ Tr 𝑢 ) → 𝑢 ∈ ∩ 𝑧 ) ) → ( ∩ 𝑧 ⊆ 𝑡 → ( 𝑡 ∈ ∩ 𝑧 → ∩ 𝑧 = 𝑡 ) ) )
23 con3 ⊢ ( ( 𝑡 ∈ ∩ 𝑧 → ∩ 𝑧 = 𝑡 ) → ( ¬ ∩ 𝑧 = 𝑡 → ¬ 𝑡 ∈ ∩ 𝑧 ) )
24 22 23 syl6 ⊢ ( ( ∩ 𝑧 ∈ V ∧ ∀ 𝑢 ( ( 𝑢 ⊊ ∩ 𝑧 ∧ Tr 𝑢 ) → 𝑢 ∈ ∩ 𝑧 ) ) → ( ∩ 𝑧 ⊆ 𝑡 → ( ¬ ∩ 𝑧 = 𝑡 → ¬ 𝑡 ∈ ∩ 𝑧 ) ) )
25 24 com23 ⊢ ( ( ∩ 𝑧 ∈ V ∧ ∀ 𝑢 ( ( 𝑢 ⊊ ∩ 𝑧 ∧ Tr 𝑢 ) → 𝑢 ∈ ∩ 𝑧 ) ) → ( ¬ ∩ 𝑧 = 𝑡 → ( ∩ 𝑧 ⊆ 𝑡 → ¬ 𝑡 ∈ ∩ 𝑧 ) ) )
26 15 25 pm2.61d ⊢ ( ( ∩ 𝑧 ∈ V ∧ ∀ 𝑢 ( ( 𝑢 ⊊ ∩ 𝑧 ∧ Tr 𝑢 ) → 𝑢 ∈ ∩ 𝑧 ) ) → ( ∩ 𝑧 ⊆ 𝑡 → ¬ 𝑡 ∈ ∩ 𝑧 ) )
27 6 26 sylanb ⊢ ( ( 𝑧 ≠ ∅ ∧ ∀ 𝑢 ( ( 𝑢 ⊊ ∩ 𝑧 ∧ Tr 𝑢 ) → 𝑢 ∈ ∩ 𝑧 ) ) → ( ∩ 𝑧 ⊆ 𝑡 → ¬ 𝑡 ∈ ∩ 𝑧 ) )
28 5 27 syldan ⊢ ( ( 𝑧 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑧 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑥 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑥 ) ) → ( ∩ 𝑧 ⊆ 𝑡 → ¬ 𝑡 ∈ ∩ 𝑧 ) )
29 4 28 syl5 ⊢ ( ( 𝑧 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑧 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑥 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑥 ) ) → ( 𝑡 ∈ 𝑧 → ¬ 𝑡 ∈ ∩ 𝑧 ) )
30 29 ralrimiv ⊢ ( ( 𝑧 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑧 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑥 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑥 ) ) → ∀ 𝑡 ∈ 𝑧 ¬ 𝑡 ∈ ∩ 𝑧 )
31 eleq2 ⊢ ( 𝑤 = ∩ 𝑧 → ( 𝑡 ∈ 𝑤 ↔ 𝑡 ∈ ∩ 𝑧 ) )
32 31 notbid ⊢ ( 𝑤 = ∩ 𝑧 → ( ¬ 𝑡 ∈ 𝑤 ↔ ¬ 𝑡 ∈ ∩ 𝑧 ) )
33 32 ralbidv ⊢ ( 𝑤 = ∩ 𝑧 → ( ∀ 𝑡 ∈ 𝑧 ¬ 𝑡 ∈ 𝑤 ↔ ∀ 𝑡 ∈ 𝑧 ¬ 𝑡 ∈ ∩ 𝑧 ) )
34 33 rspcev ⊢ ( ( ∩ 𝑧 ∈ 𝑧 ∧ ∀ 𝑡 ∈ 𝑧 ¬ 𝑡 ∈ ∩ 𝑧 ) → ∃ 𝑤 ∈ 𝑧 ∀ 𝑡 ∈ 𝑧 ¬ 𝑡 ∈ 𝑤 )
35 3 30 34 syl2anc ⊢ ( ( 𝑧 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑧 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑥 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑥 ) ) → ∃ 𝑤 ∈ 𝑧 ∀ 𝑡 ∈ 𝑧 ¬ 𝑡 ∈ 𝑤 )
36 35 expcom ⊢ ( ∀ 𝑥 ∈ 𝑧 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑥 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑥 ) → ( 𝑧 ≠ ∅ → ∃ 𝑤 ∈ 𝑧 ∀ 𝑡 ∈ 𝑧 ¬ 𝑡 ∈ 𝑤 ) )
37 1 36 syl6com ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑥 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑥 ) → ( 𝑧 ⊆ 𝐴 → ( 𝑧 ≠ ∅ → ∃ 𝑤 ∈ 𝑧 ∀ 𝑡 ∈ 𝑧 ¬ 𝑡 ∈ 𝑤 ) ) )
38 37 impd ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑥 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑥 ) → ( ( 𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅ ) → ∃ 𝑤 ∈ 𝑧 ∀ 𝑡 ∈ 𝑧 ¬ 𝑡 ∈ 𝑤 ) )
39 38 alrimiv ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑥 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑥 ) → ∀ 𝑧 ( ( 𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅ ) → ∃ 𝑤 ∈ 𝑧 ∀ 𝑡 ∈ 𝑧 ¬ 𝑡 ∈ 𝑤 ) )
40 df-fr ⊢ ( E Fr 𝐴 ↔ ∀ 𝑧 ( ( 𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅ ) → ∃ 𝑤 ∈ 𝑧 ∀ 𝑡 ∈ 𝑧 ¬ 𝑡 E 𝑤 ) )
41 epel ⊢ ( 𝑡 E 𝑤 ↔ 𝑡 ∈ 𝑤 )
42 41 notbii ⊢ ( ¬ 𝑡 E 𝑤 ↔ ¬ 𝑡 ∈ 𝑤 )
43 42 ralbii ⊢ ( ∀ 𝑡 ∈ 𝑧 ¬ 𝑡 E 𝑤 ↔ ∀ 𝑡 ∈ 𝑧 ¬ 𝑡 ∈ 𝑤 )
44 43 rexbii ⊢ ( ∃ 𝑤 ∈ 𝑧 ∀ 𝑡 ∈ 𝑧 ¬ 𝑡 E 𝑤 ↔ ∃ 𝑤 ∈ 𝑧 ∀ 𝑡 ∈ 𝑧 ¬ 𝑡 ∈ 𝑤 )
45 44 imbi2i ⊢ ( ( ( 𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅ ) → ∃ 𝑤 ∈ 𝑧 ∀ 𝑡 ∈ 𝑧 ¬ 𝑡 E 𝑤 ) ↔ ( ( 𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅ ) → ∃ 𝑤 ∈ 𝑧 ∀ 𝑡 ∈ 𝑧 ¬ 𝑡 ∈ 𝑤 ) )
46 45 albii ⊢ ( ∀ 𝑧 ( ( 𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅ ) → ∃ 𝑤 ∈ 𝑧 ∀ 𝑡 ∈ 𝑧 ¬ 𝑡 E 𝑤 ) ↔ ∀ 𝑧 ( ( 𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅ ) → ∃ 𝑤 ∈ 𝑧 ∀ 𝑡 ∈ 𝑧 ¬ 𝑡 ∈ 𝑤 ) )
47 40 46 bitri ⊢ ( E Fr 𝐴 ↔ ∀ 𝑧 ( ( 𝑧 ⊆ 𝐴 ∧ 𝑧 ≠ ∅ ) → ∃ 𝑤 ∈ 𝑧 ∀ 𝑡 ∈ 𝑧 ¬ 𝑡 ∈ 𝑤 ) )
48 39 47 sylibr ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ( ( 𝑦 ⊊ 𝑥 ∧ Tr 𝑦 ) → 𝑦 ∈ 𝑥 ) → E Fr 𝐴 )