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	syl5bi	⊢ ( 𝑥 ⊆ On → ( 𝑥 ≠ ∅ → ∃ 𝑧 ∈ 𝑥 ( 𝑥 ∩ 𝑧 ) = ∅ ) )
37	36	imp	⊢ ( ( 𝑥 ⊆ On ∧ 𝑥 ≠ ∅ ) → ∃ 𝑧 ∈ 𝑥 ( 𝑥 ∩ 𝑧 ) = ∅ )
38	1 37	mpgbir	⊢ E Fr On