Theorem onfr 6353

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

Assertion

Ref	Expression
onfr	⊢ E Fr On

Proof of Theorem onfr

Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		dfepfr 5605	. 2 ⊢ ( E Fr On ↔ ∀𝑥((𝑥 ⊆ On ∧ 𝑥 ≠ ∅) → ∃𝑧 ∈ 𝑥 (𝑥 ∩ 𝑧) = ∅))
2		n0 4284	. . . 4 ⊢ (𝑥 ≠ ∅ ↔ ∃𝑦 𝑦 ∈ 𝑥)
3		ineq2 4146	. . . . . . . . . 10 ⊢ (𝑧 = 𝑦 → (𝑥 ∩ 𝑧) = (𝑥 ∩ 𝑦))
4	3	eqeq1d 2743	. . . . . . . . 9 ⊢ (𝑧 = 𝑦 → ((𝑥 ∩ 𝑧) = ∅ ↔ (𝑥 ∩ 𝑦) = ∅))
5	4	rspcev 3562	. . . . . . . 8 ⊢ ((𝑦 ∈ 𝑥 ∧ (𝑥 ∩ 𝑦) = ∅) → ∃𝑧 ∈ 𝑥 (𝑥 ∩ 𝑧) = ∅)
6	5	adantll 721	. . . . . . 7 ⊢ (((𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥) ∧ (𝑥 ∩ 𝑦) = ∅) → ∃𝑧 ∈ 𝑥 (𝑥 ∩ 𝑧) = ∅)
7		inss1 4168	. . . . . . . 8 ⊢ (𝑥 ∩ 𝑦) ⊆ 𝑥
8		ssel2 3912	. . . . . . . . . . 11 ⊢ ((𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ On)
9		eloni 6324	. . . . . . . . . . 11 ⊢ (𝑦 ∈ On → Ord 𝑦)
10		ordfr 6329	. . . . . . . . . . 11 ⊢ (Ord 𝑦 → E Fr 𝑦)
11	8, 9, 10	3syl 18	. . . . . . . . . 10 ⊢ ((𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥) → E Fr 𝑦)
12		inss2 4169	. . . . . . . . . . 11 ⊢ (𝑥 ∩ 𝑦) ⊆ 𝑦
13		vex 3437	. . . . . . . . . . . . 13 ⊢ 𝑥 ∈ V
14	13	inex1 5248	. . . . . . . . . . . 12 ⊢ (𝑥 ∩ 𝑦) ∈ V
15	14	epfrc 5606	. . . . . . . . . . 11 ⊢ (( E Fr 𝑦 ∧ (𝑥 ∩ 𝑦) ⊆ 𝑦 ∧ (𝑥 ∩ 𝑦) ≠ ∅) → ∃𝑧 ∈ (𝑥 ∩ 𝑦)((𝑥 ∩ 𝑦) ∩ 𝑧) = ∅)
16	12, 15	mp3an2 1458	. . . . . . . . . 10 ⊢ (( E Fr 𝑦 ∧ (𝑥 ∩ 𝑦) ≠ ∅) → ∃𝑧 ∈ (𝑥 ∩ 𝑦)((𝑥 ∩ 𝑦) ∩ 𝑧) = ∅)
17	11, 16	sylan 587	. . . . . . . . 9 ⊢ (((𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥) ∧ (𝑥 ∩ 𝑦) ≠ ∅) → ∃𝑧 ∈ (𝑥 ∩ 𝑦)((𝑥 ∩ 𝑦) ∩ 𝑧) = ∅)
18		inass 4159	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∩ 𝑦) ∩ 𝑧) = (𝑥 ∩ (𝑦 ∩ 𝑧))
19	8, 9	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥) → Ord 𝑦)
20		elinel2 4134	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ (𝑥 ∩ 𝑦) → 𝑧 ∈ 𝑦)
21		ordelss 6330	. . . . . . . . . . . . . . . 16 ⊢ ((Ord 𝑦 ∧ 𝑧 ∈ 𝑦) → 𝑧 ⊆ 𝑦)
22	19, 20, 21	syl2an 603	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥) ∧ 𝑧 ∈ (𝑥 ∩ 𝑦)) → 𝑧 ⊆ 𝑦)
23		sseqin2 4155	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ⊆ 𝑦 ↔ (𝑦 ∩ 𝑧) = 𝑧)
24	22, 23	sylib 220	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥) ∧ 𝑧 ∈ (𝑥 ∩ 𝑦)) → (𝑦 ∩ 𝑧) = 𝑧)
25	24	ineq2d 4152	. . . . . . . . . . . . 13 ⊢ (((𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥) ∧ 𝑧 ∈ (𝑥 ∩ 𝑦)) → (𝑥 ∩ (𝑦 ∩ 𝑧)) = (𝑥 ∩ 𝑧))
26	18, 25	eqtrid 2788	. . . . . . . . . . . 12 ⊢ (((𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥) ∧ 𝑧 ∈ (𝑥 ∩ 𝑦)) → ((𝑥 ∩ 𝑦) ∩ 𝑧) = (𝑥 ∩ 𝑧))
27	26	eqeq1d 2743	. . . . . . . . . . 11 ⊢ (((𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥) ∧ 𝑧 ∈ (𝑥 ∩ 𝑦)) → (((𝑥 ∩ 𝑦) ∩ 𝑧) = ∅ ↔ (𝑥 ∩ 𝑧) = ∅))
28	27	rexbidva 3163	. . . . . . . . . 10 ⊢ ((𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥) → (∃𝑧 ∈ (𝑥 ∩ 𝑦)((𝑥 ∩ 𝑦) ∩ 𝑧) = ∅ ↔ ∃𝑧 ∈ (𝑥 ∩ 𝑦)(𝑥 ∩ 𝑧) = ∅))
29	28	adantr 482	. . . . . . . . 9 ⊢ (((𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥) ∧ (𝑥 ∩ 𝑦) ≠ ∅) → (∃𝑧 ∈ (𝑥 ∩ 𝑦)((𝑥 ∩ 𝑦) ∩ 𝑧) = ∅ ↔ ∃𝑧 ∈ (𝑥 ∩ 𝑦)(𝑥 ∩ 𝑧) = ∅))
30	17, 29	mpbid 234	. . . . . . . 8 ⊢ (((𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥) ∧ (𝑥 ∩ 𝑦) ≠ ∅) → ∃𝑧 ∈ (𝑥 ∩ 𝑦)(𝑥 ∩ 𝑧) = ∅)
31		ssrexv 3987	. . . . . . . 8 ⊢ ((𝑥 ∩ 𝑦) ⊆ 𝑥 → (∃𝑧 ∈ (𝑥 ∩ 𝑦)(𝑥 ∩ 𝑧) = ∅ → ∃𝑧 ∈ 𝑥 (𝑥 ∩ 𝑧) = ∅))
32	7, 30, 31	mpsyl 68	. . . . . . 7 ⊢ (((𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥) ∧ (𝑥 ∩ 𝑦) ≠ ∅) → ∃𝑧 ∈ 𝑥 (𝑥 ∩ 𝑧) = ∅)
33	6, 32	pm2.61dane 3023	. . . . . 6 ⊢ ((𝑥 ⊆ On ∧ 𝑦 ∈ 𝑥) → ∃𝑧 ∈ 𝑥 (𝑥 ∩ 𝑧) = ∅)
34	33	ex 414	. . . . 5 ⊢ (𝑥 ⊆ On → (𝑦 ∈ 𝑥 → ∃𝑧 ∈ 𝑥 (𝑥 ∩ 𝑧) = ∅))
35	34	exlimdv 1941	. . . 4 ⊢ (𝑥 ⊆ On → (∃𝑦 𝑦 ∈ 𝑥 → ∃𝑧 ∈ 𝑥 (𝑥 ∩ 𝑧) = ∅))
36	2, 35	biimtrid 244	. . 3 ⊢ (𝑥 ⊆ On → (𝑥 ≠ ∅ → ∃𝑧 ∈ 𝑥 (𝑥 ∩ 𝑧) = ∅))
37	36	imp 408	. 2 ⊢ ((𝑥 ⊆ On ∧ 𝑥 ≠ ∅) → ∃𝑧 ∈ 𝑥 (𝑥 ∩ 𝑧) = ∅)
38	1, 37	mpgbir 1807	1 ⊢ E Fr On

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 397   = wceq 1548  ∃wex 1787   ∈ wcel 2121   ≠ wne 2936  ∃wrex 3065   ∩ cin 3884   ⊆ wss 3885  ∅c0 4264   E cep 5520   Fr wfr 5571  Ord word 6313  Oncon0 6314

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713  ax-sep 5221  ax-pr 5365

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-ne 2937  df-ral 3056  df-rex 3066  df-rab 3394  df-v 3435  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-nul 4265  df-if 4458  df-pw 4534  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4842  df-br 5076  df-opab 5138  df-tr 5183  df-eprel 5521  df-po 5529  df-so 5530  df-fr 5574  df-we 5576  df-ord 6317  df-on 6318

This theorem is referenced by:  epweon  7722  epweonALT  7723  on2recsfn  8597  on2recsov  8598  on2ind  8599  on3ind  8600  wffr  45420