Theorem onfrALT

Description: The membership relation is foundational on the class of ordinal numbers. onfrALT is an alternate proof of onfr . onfrALTVD is the Virtual Deduction proof from which onfrALT is derived. The Virtual Deduction proof mirrors the working proof of onfr which is the main part of the proof of Theorem 7.12 of the first edition of TakeutiZaring. The proof of the corresponding Proposition 7.12 of TakeutiZaring p. 38 (second edition) does not contain the working proof equivalent of onfrALTVD . This theorem does not rely on the Axiom of Regularity. (Contributed by Alan Sare, 22-Jul-2012) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	onfrALT	⊢ E Fr On

Proof

Step	Hyp	Ref	Expression
1		dfepfr	⊢ ( E Fr On ↔ ∀ 𝑎 ( ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑎 ( 𝑎 ∩ 𝑦 ) = ∅ ) )
2		simpr	⊢ ( ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ ) → 𝑎 ≠ ∅ )
3		n0	⊢ ( 𝑎 ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ 𝑎 )
4		onfrALTlem1	⊢ ( ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ ) → ( ( 𝑥 ∈ 𝑎 ∧ ( 𝑎 ∩ 𝑥 ) = ∅ ) → ∃ 𝑦 ∈ 𝑎 ( 𝑎 ∩ 𝑦 ) = ∅ ) )
5	4	expd	⊢ ( ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ ) → ( 𝑥 ∈ 𝑎 → ( ( 𝑎 ∩ 𝑥 ) = ∅ → ∃ 𝑦 ∈ 𝑎 ( 𝑎 ∩ 𝑦 ) = ∅ ) ) )
6		onfrALTlem2	⊢ ( ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ ) → ( ( 𝑥 ∈ 𝑎 ∧ ¬ ( 𝑎 ∩ 𝑥 ) = ∅ ) → ∃ 𝑦 ∈ 𝑎 ( 𝑎 ∩ 𝑦 ) = ∅ ) )
7	6	expd	⊢ ( ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ ) → ( 𝑥 ∈ 𝑎 → ( ¬ ( 𝑎 ∩ 𝑥 ) = ∅ → ∃ 𝑦 ∈ 𝑎 ( 𝑎 ∩ 𝑦 ) = ∅ ) ) )
8		pm2.61	⊢ ( ( ( 𝑎 ∩ 𝑥 ) = ∅ → ∃ 𝑦 ∈ 𝑎 ( 𝑎 ∩ 𝑦 ) = ∅ ) → ( ( ¬ ( 𝑎 ∩ 𝑥 ) = ∅ → ∃ 𝑦 ∈ 𝑎 ( 𝑎 ∩ 𝑦 ) = ∅ ) → ∃ 𝑦 ∈ 𝑎 ( 𝑎 ∩ 𝑦 ) = ∅ ) )
9	5 7 8	syl6c	⊢ ( ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ ) → ( 𝑥 ∈ 𝑎 → ∃ 𝑦 ∈ 𝑎 ( 𝑎 ∩ 𝑦 ) = ∅ ) )
10	9	exlimdv	⊢ ( ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ ) → ( ∃ 𝑥 𝑥 ∈ 𝑎 → ∃ 𝑦 ∈ 𝑎 ( 𝑎 ∩ 𝑦 ) = ∅ ) )
11	3 10	syl5bi	⊢ ( ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ ) → ( 𝑎 ≠ ∅ → ∃ 𝑦 ∈ 𝑎 ( 𝑎 ∩ 𝑦 ) = ∅ ) )
12	2 11	mpd	⊢ ( ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑎 ( 𝑎 ∩ 𝑦 ) = ∅ )
13	1 12	mpgbir	⊢ E Fr On