This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem onfr

Description: The ordinal class is well-founded. This proof does not require the axiom of regularity. This lemma is used in ordon (through epweon ) in order to eliminate the need for the axiom of regularity. (Contributed by NM, 17-May-1994)

Ref Expression
Assertion onfr E Fr On

Proof

Step Hyp Ref Expression
1 dfepfr ⊢ ( E Fr On ↔ ∀ 𝑥 ( ( 𝑥 ⊆ On ∧ 𝑥 ≠ ∅ ) → ∃ 𝑧 ∈ 𝑥 ( 𝑥 ∩ 𝑧 ) = ∅ ) )
2 n0 ⊢ ( 𝑥 ≠ ∅ ↔ ∃ 𝑦 𝑦 ∈ 𝑥 )
3 ineq2 ⊢ ( 𝑧 = 𝑦 → ( 𝑥 ∩ 𝑧 ) = ( 𝑥 ∩ 𝑦 ) )
4 3 eqeq1d ⊢ ( 𝑧 = 𝑦 → ( ( 𝑥 ∩ 𝑧 ) = ∅ ↔ ( 𝑥 ∩ 𝑦 ) = ∅ ) )
5 4 rspcev ⊢ ( ( 𝑦 ∈ 𝑥 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) → ∃ 𝑧 ∈ 𝑥 ( 𝑥 ∩ 𝑧 ) = ∅ )
6 5 adantll ⊢ ( ( ( 𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) → ∃ 𝑧 ∈ 𝑥 ( 𝑥 ∩ 𝑧 ) = ∅ )
7 inss1 ⊢ ( 𝑥 ∩ 𝑦 ) ⊆ 𝑥
8 ssel2 ⊢ ( ( 𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ On )
9 eloni ⊢ ( 𝑦 ∈ On → Ord 𝑦 )
10 ordfr ⊢ ( Ord 𝑦 → E Fr 𝑦 )
11 8 9 10 3syl ⊢ ( ( 𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥 ) → E Fr 𝑦 )
12 inss2 ⊢ ( 𝑥 ∩ 𝑦 ) ⊆ 𝑦
13 vex ⊢ 𝑥 ∈ V
14 13 inex1 ⊢ ( 𝑥 ∩ 𝑦 ) ∈ V
15 14 epfrc ⊢ ( ( E Fr 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) ⊆ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) ≠ ∅ ) → ∃ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ( ( 𝑥 ∩ 𝑦 ) ∩ 𝑧 ) = ∅ )
16 12 15 mp3an2 ⊢ ( ( E Fr 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) ≠ ∅ ) → ∃ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ( ( 𝑥 ∩ 𝑦 ) ∩ 𝑧 ) = ∅ )
17 11 16 sylan ⊢ ( ( ( 𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑥 ∩ 𝑦 ) ≠ ∅ ) → ∃ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ( ( 𝑥 ∩ 𝑦 ) ∩ 𝑧 ) = ∅ )
18 inass ⊢ ( ( 𝑥 ∩ 𝑦 ) ∩ 𝑧 ) = ( 𝑥 ∩ ( 𝑦 ∩ 𝑧 ) )
19 8 9 syl ⊢ ( ( 𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥 ) → Ord 𝑦 )
20 elinel2 ⊢ ( 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) → 𝑧 ∈ 𝑦 )
21 ordelss ⊢ ( ( Ord 𝑦 ∧ 𝑧 ∈ 𝑦 ) → 𝑧 ⊆ 𝑦 )
22 19 20 21 syl2an ⊢ ( ( ( 𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) → 𝑧 ⊆ 𝑦 )
23 sseqin2 ⊢ ( 𝑧 ⊆ 𝑦 ↔ ( 𝑦 ∩ 𝑧 ) = 𝑧 )
24 22 23 sylib ⊢ ( ( ( 𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) → ( 𝑦 ∩ 𝑧 ) = 𝑧 )
25 24 ineq2d ⊢ ( ( ( 𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) → ( 𝑥 ∩ ( 𝑦 ∩ 𝑧 ) ) = ( 𝑥 ∩ 𝑧 ) )
26 18 25 eqtrid ⊢ ( ( ( 𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) → ( ( 𝑥 ∩ 𝑦 ) ∩ 𝑧 ) = ( 𝑥 ∩ 𝑧 ) )
27 26 eqeq1d ⊢ ( ( ( 𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥 ) ∧ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ) → ( ( ( 𝑥 ∩ 𝑦 ) ∩ 𝑧 ) = ∅ ↔ ( 𝑥 ∩ 𝑧 ) = ∅ ) )
28 27 rexbidva ⊢ ( ( 𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥 ) → ( ∃ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ( ( 𝑥 ∩ 𝑦 ) ∩ 𝑧 ) = ∅ ↔ ∃ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ( 𝑥 ∩ 𝑧 ) = ∅ ) )
29 28 adantr ⊢ ( ( ( 𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑥 ∩ 𝑦 ) ≠ ∅ ) → ( ∃ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ( ( 𝑥 ∩ 𝑦 ) ∩ 𝑧 ) = ∅ ↔ ∃ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ( 𝑥 ∩ 𝑧 ) = ∅ ) )
30 17 29 mpbid ⊢ ( ( ( 𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑥 ∩ 𝑦 ) ≠ ∅ ) → ∃ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ( 𝑥 ∩ 𝑧 ) = ∅ )
31 ssrexv ⊢ ( ( 𝑥 ∩ 𝑦 ) ⊆ 𝑥 → ( ∃ 𝑧 ∈ ( 𝑥 ∩ 𝑦 ) ( 𝑥 ∩ 𝑧 ) = ∅ → ∃ 𝑧 ∈ 𝑥 ( 𝑥 ∩ 𝑧 ) = ∅ ) )
32 7 30 31 mpsyl ⊢ ( ( ( 𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥 ) ∧ ( 𝑥 ∩ 𝑦 ) ≠ ∅ ) → ∃ 𝑧 ∈ 𝑥 ( 𝑥 ∩ 𝑧 ) = ∅ )
33 6 32 pm2.61dane ⊢ ( ( 𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥 ) → ∃ 𝑧 ∈ 𝑥 ( 𝑥 ∩ 𝑧 ) = ∅ )
34 33 ex ⊢ ( 𝑥 ⊆ On → ( 𝑦 ∈ 𝑥 → ∃ 𝑧 ∈ 𝑥 ( 𝑥 ∩ 𝑧 ) = ∅ ) )
35 34 exlimdv ⊢ ( 𝑥 ⊆ On → ( ∃ 𝑦 𝑦 ∈ 𝑥 → ∃ 𝑧 ∈ 𝑥 ( 𝑥 ∩ 𝑧 ) = ∅ ) )
36 2 35 biimtrid ⊢ ( 𝑥 ⊆ On → ( 𝑥 ≠ ∅ → ∃ 𝑧 ∈ 𝑥 ( 𝑥 ∩ 𝑧 ) = ∅ ) )
37 36 imp ⊢ ( ( 𝑥 ⊆ On ∧ 𝑥 ≠ ∅ ) → ∃ 𝑧 ∈ 𝑥 ( 𝑥 ∩ 𝑧 ) = ∅ )
38 1 37 mpgbir ⊢ E Fr On