Metamath Proof Explorer


Theorem onfrALTlem3

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

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

Proof

Step Hyp Ref Expression
1 ssid ( 𝑎𝑥 ) ⊆ ( 𝑎𝑥 )
2 simpr ( ( 𝑥𝑎 ∧ ¬ ( 𝑎𝑥 ) = ∅ ) → ¬ ( 𝑎𝑥 ) = ∅ )
3 2 a1i ( ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ ) → ( ( 𝑥𝑎 ∧ ¬ ( 𝑎𝑥 ) = ∅ ) → ¬ ( 𝑎𝑥 ) = ∅ ) )
4 df-ne ( ( 𝑎𝑥 ) ≠ ∅ ↔ ¬ ( 𝑎𝑥 ) = ∅ )
5 3 4 syl6ibr ( ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ ) → ( ( 𝑥𝑎 ∧ ¬ ( 𝑎𝑥 ) = ∅ ) → ( 𝑎𝑥 ) ≠ ∅ ) )
6 pm3.2 ( ( 𝑎𝑥 ) ⊆ ( 𝑎𝑥 ) → ( ( 𝑎𝑥 ) ≠ ∅ → ( ( 𝑎𝑥 ) ⊆ ( 𝑎𝑥 ) ∧ ( 𝑎𝑥 ) ≠ ∅ ) ) )
7 1 5 6 mpsylsyld ( ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ ) → ( ( 𝑥𝑎 ∧ ¬ ( 𝑎𝑥 ) = ∅ ) → ( ( 𝑎𝑥 ) ⊆ ( 𝑎𝑥 ) ∧ ( 𝑎𝑥 ) ≠ ∅ ) ) )
8 vex 𝑥 ∈ V
9 8 inex2 ( 𝑎𝑥 ) ∈ V
10 inss2 ( 𝑎𝑥 ) ⊆ 𝑥
11 simpl ( ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ ) → 𝑎 ⊆ On )
12 simpl ( ( 𝑥𝑎 ∧ ¬ ( 𝑎𝑥 ) = ∅ ) → 𝑥𝑎 )
13 ssel ( 𝑎 ⊆ On → ( 𝑥𝑎𝑥 ∈ On ) )
14 11 12 13 syl2im ( ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ ) → ( ( 𝑥𝑎 ∧ ¬ ( 𝑎𝑥 ) = ∅ ) → 𝑥 ∈ On ) )
15 eloni ( 𝑥 ∈ On → Ord 𝑥 )
16 14 15 syl6 ( ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ ) → ( ( 𝑥𝑎 ∧ ¬ ( 𝑎𝑥 ) = ∅ ) → Ord 𝑥 ) )
17 ordwe ( Ord 𝑥 → E We 𝑥 )
18 16 17 syl6 ( ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ ) → ( ( 𝑥𝑎 ∧ ¬ ( 𝑎𝑥 ) = ∅ ) → E We 𝑥 ) )
19 wess ( ( 𝑎𝑥 ) ⊆ 𝑥 → ( E We 𝑥 → E We ( 𝑎𝑥 ) ) )
20 10 18 19 mpsylsyld ( ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ ) → ( ( 𝑥𝑎 ∧ ¬ ( 𝑎𝑥 ) = ∅ ) → E We ( 𝑎𝑥 ) ) )
21 wefr ( E We ( 𝑎𝑥 ) → E Fr ( 𝑎𝑥 ) )
22 20 21 syl6 ( ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ ) → ( ( 𝑥𝑎 ∧ ¬ ( 𝑎𝑥 ) = ∅ ) → E Fr ( 𝑎𝑥 ) ) )
23 dfepfr ( E Fr ( 𝑎𝑥 ) ↔ ∀ 𝑏 ( ( 𝑏 ⊆ ( 𝑎𝑥 ) ∧ 𝑏 ≠ ∅ ) → ∃ 𝑦𝑏 ( 𝑏𝑦 ) = ∅ ) )
24 22 23 syl6ib ( ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ ) → ( ( 𝑥𝑎 ∧ ¬ ( 𝑎𝑥 ) = ∅ ) → ∀ 𝑏 ( ( 𝑏 ⊆ ( 𝑎𝑥 ) ∧ 𝑏 ≠ ∅ ) → ∃ 𝑦𝑏 ( 𝑏𝑦 ) = ∅ ) ) )
25 spsbc ( ( 𝑎𝑥 ) ∈ V → ( ∀ 𝑏 ( ( 𝑏 ⊆ ( 𝑎𝑥 ) ∧ 𝑏 ≠ ∅ ) → ∃ 𝑦𝑏 ( 𝑏𝑦 ) = ∅ ) → [ ( 𝑎𝑥 ) / 𝑏 ] ( ( 𝑏 ⊆ ( 𝑎𝑥 ) ∧ 𝑏 ≠ ∅ ) → ∃ 𝑦𝑏 ( 𝑏𝑦 ) = ∅ ) ) )
26 9 24 25 mpsylsyld ( ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ ) → ( ( 𝑥𝑎 ∧ ¬ ( 𝑎𝑥 ) = ∅ ) → [ ( 𝑎𝑥 ) / 𝑏 ] ( ( 𝑏 ⊆ ( 𝑎𝑥 ) ∧ 𝑏 ≠ ∅ ) → ∃ 𝑦𝑏 ( 𝑏𝑦 ) = ∅ ) ) )
27 onfrALTlem5 ( [ ( 𝑎𝑥 ) / 𝑏 ] ( ( 𝑏 ⊆ ( 𝑎𝑥 ) ∧ 𝑏 ≠ ∅ ) → ∃ 𝑦𝑏 ( 𝑏𝑦 ) = ∅ ) ↔ ( ( ( 𝑎𝑥 ) ⊆ ( 𝑎𝑥 ) ∧ ( 𝑎𝑥 ) ≠ ∅ ) → ∃ 𝑦 ∈ ( 𝑎𝑥 ) ( ( 𝑎𝑥 ) ∩ 𝑦 ) = ∅ ) )
28 26 27 syl6ib ( ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ ) → ( ( 𝑥𝑎 ∧ ¬ ( 𝑎𝑥 ) = ∅ ) → ( ( ( 𝑎𝑥 ) ⊆ ( 𝑎𝑥 ) ∧ ( 𝑎𝑥 ) ≠ ∅ ) → ∃ 𝑦 ∈ ( 𝑎𝑥 ) ( ( 𝑎𝑥 ) ∩ 𝑦 ) = ∅ ) ) )
29 7 28 mpdd ( ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ ) → ( ( 𝑥𝑎 ∧ ¬ ( 𝑎𝑥 ) = ∅ ) → ∃ 𝑦 ∈ ( 𝑎𝑥 ) ( ( 𝑎𝑥 ) ∩ 𝑦 ) = ∅ ) )