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

Metamath Proof Explorer

Theorem onfrALTlem1

Description: Lemma for onfrALT . (Contributed by Alan Sare, 22-Jul-2012) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion onfrALTlem1 ( ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ ) → ( ( 𝑥 ∈ 𝑎 ∧ ( 𝑎 ∩ 𝑥 ) = ∅ ) → ∃ 𝑦 ∈ 𝑎 ( 𝑎 ∩ 𝑦 ) = ∅ ) )

Proof

Step Hyp Ref Expression
1 19.8a ⊢ ( ( 𝑥 ∈ 𝑎 ∧ ( 𝑎 ∩ 𝑥 ) = ∅ ) → ∃ 𝑥 ( 𝑥 ∈ 𝑎 ∧ ( 𝑎 ∩ 𝑥 ) = ∅ ) )
2 1 a1i ⊢ ( ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ ) → ( ( 𝑥 ∈ 𝑎 ∧ ( 𝑎 ∩ 𝑥 ) = ∅ ) → ∃ 𝑥 ( 𝑥 ∈ 𝑎 ∧ ( 𝑎 ∩ 𝑥 ) = ∅ ) ) )
3 cbvexsv ⊢ ( ∃ 𝑥 ( 𝑥 ∈ 𝑎 ∧ ( 𝑎 ∩ 𝑥 ) = ∅ ) ↔ ∃ 𝑦 [ 𝑦 / 𝑥 ] ( 𝑥 ∈ 𝑎 ∧ ( 𝑎 ∩ 𝑥 ) = ∅ ) )
4 2 3 imbitrdi ⊢ ( ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ ) → ( ( 𝑥 ∈ 𝑎 ∧ ( 𝑎 ∩ 𝑥 ) = ∅ ) → ∃ 𝑦 [ 𝑦 / 𝑥 ] ( 𝑥 ∈ 𝑎 ∧ ( 𝑎 ∩ 𝑥 ) = ∅ ) ) )
5 sbsbc ⊢ ( [ 𝑦 / 𝑥 ] ( 𝑥 ∈ 𝑎 ∧ ( 𝑎 ∩ 𝑥 ) = ∅ ) ↔ [ 𝑦 / 𝑥 ] ( 𝑥 ∈ 𝑎 ∧ ( 𝑎 ∩ 𝑥 ) = ∅ ) )
6 onfrALTlem4 ⊢ ( [ 𝑦 / 𝑥 ] ( 𝑥 ∈ 𝑎 ∧ ( 𝑎 ∩ 𝑥 ) = ∅ ) ↔ ( 𝑦 ∈ 𝑎 ∧ ( 𝑎 ∩ 𝑦 ) = ∅ ) )
7 5 6 bitri ⊢ ( [ 𝑦 / 𝑥 ] ( 𝑥 ∈ 𝑎 ∧ ( 𝑎 ∩ 𝑥 ) = ∅ ) ↔ ( 𝑦 ∈ 𝑎 ∧ ( 𝑎 ∩ 𝑦 ) = ∅ ) )
8 7 exbii ⊢ ( ∃ 𝑦 [ 𝑦 / 𝑥 ] ( 𝑥 ∈ 𝑎 ∧ ( 𝑎 ∩ 𝑥 ) = ∅ ) ↔ ∃ 𝑦 ( 𝑦 ∈ 𝑎 ∧ ( 𝑎 ∩ 𝑦 ) = ∅ ) )
9 4 8 imbitrdi ⊢ ( ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ ) → ( ( 𝑥 ∈ 𝑎 ∧ ( 𝑎 ∩ 𝑥 ) = ∅ ) → ∃ 𝑦 ( 𝑦 ∈ 𝑎 ∧ ( 𝑎 ∩ 𝑦 ) = ∅ ) ) )
10 df-rex ⊢ ( ∃ 𝑦 ∈ 𝑎 ( 𝑎 ∩ 𝑦 ) = ∅ ↔ ∃ 𝑦 ( 𝑦 ∈ 𝑎 ∧ ( 𝑎 ∩ 𝑦 ) = ∅ ) )
11 9 10 imbitrrdi ⊢ ( ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ ) → ( ( 𝑥 ∈ 𝑎 ∧ ( 𝑎 ∩ 𝑥 ) = ∅ ) → ∃ 𝑦 ∈ 𝑎 ( 𝑎 ∩ 𝑦 ) = ∅ ) )