Metamath Proof Explorer

Theorem onfrALTlem3VD

Description: Virtual deduction proof of onfrALTlem3 . The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. onfrALTlem3 is onfrALTlem3VD without virtual deductions and was automatically derived from onfrALTlem3VD .

1:: |- (. ( a C_ On /\ a =/= (/) ) ->. ( a C_ On /\ a =/= (/) ) ).
2:: |- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. ( x e. a /\ -. ( a i^i x ) = (/) ) ).
3:2: |- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. x e. a ).
4:1: |- (. ( a C_ On /\ a =/= (/) ) ->. a C_ On ).
5:3,4: |- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. x e. On ).
6:5: |- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. Ord x ).
7:6: |- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->.E We x ).
8:: |- ( a i^i x ) C x
9:7,8: |- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->.E We ( a i^i x ) ).
10:9: |- (. ( a C On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->.E Fr ( a i^i x ) ).
11:10: |- (. ( a C On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. A. b ( ( b C_ ( a i^i x ) /\ b =/= (/) ) -> E. y e. b ( b i^i y ) = (/) ) ).
12:: |- x e.V
13:12,8: |- ( a i^i x ) e. V
14:13,11: |- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. [. ( a i^i x ) / b ]. ( ( b C_ ( a i^i x ) /\ b =/= (/) ) -> E. y e. b ( b i^i y ) = (/) ) ).
15:: |- ( [. ( a i^i x ) / b ]. ( ( b C_ ( a i^i x ) /\ b =/= (/) ) -> E. y e. b ( b i^i y ) = (/) ) <-> ( ( ( a i^i x ) C_ ( a i^i x ) /\ ( a i^i x ) =/= (/) ) -> E. y e. ( a i^i x ) ( ( a i^i x ) i^i y ) = (/) ) )
16:14,15: |- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. ( ( ( a i^i x ) C_ ( a i^i x ) /\ ( a i^i x ) =/= (/) ) -> E. y e. ( a i^i x ) ( ( a i^i x ) i^i y ) = (/) ) ).
17:: |- ( a i^i x ) C_ ( a i^i x )
18:2: |- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. -. ( a i^i x ) = (/) ).
19:18: |- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. ( a i^i x ) =/= (/) ).
20:17,19: |- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. ( ( a i^i x ) C_ ( a i^i x ) /\ ( a i^i x ) =/= (/) ) ).
qed:16,20: |- (. ( a C_ On /\ a =/= (/) ) ,. ( x e. a /\ -. ( a i^i x ) = (/) ) ->. E. y e. ( a i^i x ) ( ( a i^i x ) i^i y ) = (/) ).
(Contributed by Alan Sare, 22-Jul-2012) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion onfrALTlem3VD (    ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ )    ,    ( 𝑥 ∈ 𝑎 ∧ ¬ ( 𝑎 ∩ 𝑥 ) = ∅ )    ▶    ∃ 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅    )

Proof

Step Hyp Ref Expression
1 vex ⊢ 𝑥 ∈ V
2 inss2 ⊢ ( 𝑎 ∩ 𝑥 ) ⊆ 𝑥
3 1 2 ssexi ⊢ ( 𝑎 ∩ 𝑥 ) ∈ V
4 idn2 ⊢ (    ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ )    ,    ( 𝑥 ∈ 𝑎 ∧ ¬ ( 𝑎 ∩ 𝑥 ) = ∅ )    ▶    ( 𝑥 ∈ 𝑎 ∧ ¬ ( 𝑎 ∩ 𝑥 ) = ∅ )    )
5 simpl ⊢ ( ( 𝑥 ∈ 𝑎 ∧ ¬ ( 𝑎 ∩ 𝑥 ) = ∅ ) → 𝑥 ∈ 𝑎 )
6 4 5 e2 ⊢ (    ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ )    ,    ( 𝑥 ∈ 𝑎 ∧ ¬ ( 𝑎 ∩ 𝑥 ) = ∅ )    ▶    𝑥 ∈ 𝑎    )
7 idn1 ⊢ (    ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ )    ▶    ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ )    )
8 simpl ⊢ ( ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ ) → 𝑎 ⊆ On )
9 7 8 e1a ⊢ (    ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ )    ▶    𝑎 ⊆ On    )
10 ssel ⊢ ( 𝑎 ⊆ On → ( 𝑥 ∈ 𝑎 → 𝑥 ∈ On ) )
11 10 com12 ⊢ ( 𝑥 ∈ 𝑎 → ( 𝑎 ⊆ On → 𝑥 ∈ On ) )
12 6 9 11 e21 ⊢ (    ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ )    ,    ( 𝑥 ∈ 𝑎 ∧ ¬ ( 𝑎 ∩ 𝑥 ) = ∅ )    ▶    𝑥 ∈ On    )
13 eloni ⊢ ( 𝑥 ∈ On → Ord 𝑥 )
14 12 13 e2 ⊢ (    ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ )    ,    ( 𝑥 ∈ 𝑎 ∧ ¬ ( 𝑎 ∩ 𝑥 ) = ∅ )    ▶    Ord 𝑥    )
15 ordwe ⊢ ( Ord 𝑥 → E We 𝑥 )
16 14 15 e2 ⊢ (    ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ )    ,    ( 𝑥 ∈ 𝑎 ∧ ¬ ( 𝑎 ∩ 𝑥 ) = ∅ )    ▶    E We 𝑥    )
17 wess ⊢ ( ( 𝑎 ∩ 𝑥 ) ⊆ 𝑥 → ( E We 𝑥 → E We ( 𝑎 ∩ 𝑥 ) ) )
18 17 com12 ⊢ ( E We 𝑥 → ( ( 𝑎 ∩ 𝑥 ) ⊆ 𝑥 → E We ( 𝑎 ∩ 𝑥 ) ) )
19 16 2 18 e20 ⊢ (    ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ )    ,    ( 𝑥 ∈ 𝑎 ∧ ¬ ( 𝑎 ∩ 𝑥 ) = ∅ )    ▶    E We ( 𝑎 ∩ 𝑥 )    )
20 wefr ⊢ ( E We ( 𝑎 ∩ 𝑥 ) → E Fr ( 𝑎 ∩ 𝑥 ) )
21 19 20 e2 ⊢ (    ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ )    ,    ( 𝑥 ∈ 𝑎 ∧ ¬ ( 𝑎 ∩ 𝑥 ) = ∅ )    ▶    E Fr ( 𝑎 ∩ 𝑥 )    )
22 dfepfr ⊢ ( E Fr ( 𝑎 ∩ 𝑥 ) ↔ ∀ 𝑏 ( ( 𝑏 ⊆ ( 𝑎 ∩ 𝑥 ) ∧ 𝑏 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑏 ( 𝑏 ∩ 𝑦 ) = ∅ ) )
23 22 biimpi ⊢ ( E Fr ( 𝑎 ∩ 𝑥 ) → ∀ 𝑏 ( ( 𝑏 ⊆ ( 𝑎 ∩ 𝑥 ) ∧ 𝑏 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑏 ( 𝑏 ∩ 𝑦 ) = ∅ ) )
24 21 23 e2 ⊢ (    ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ )    ,    ( 𝑥 ∈ 𝑎 ∧ ¬ ( 𝑎 ∩ 𝑥 ) = ∅ )    ▶    ∀ 𝑏 ( ( 𝑏 ⊆ ( 𝑎 ∩ 𝑥 ) ∧ 𝑏 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑏 ( 𝑏 ∩ 𝑦 ) = ∅ )    )
25 spsbc ⊢ ( ( 𝑎 ∩ 𝑥 ) ∈ V → ( ∀ 𝑏 ( ( 𝑏 ⊆ ( 𝑎 ∩ 𝑥 ) ∧ 𝑏 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑏 ( 𝑏 ∩ 𝑦 ) = ∅ ) → [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] ( ( 𝑏 ⊆ ( 𝑎 ∩ 𝑥 ) ∧ 𝑏 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑏 ( 𝑏 ∩ 𝑦 ) = ∅ ) ) )
26 3 24 25 e02 ⊢ (    ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ )    ,    ( 𝑥 ∈ 𝑎 ∧ ¬ ( 𝑎 ∩ 𝑥 ) = ∅ )    ▶    [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] ( ( 𝑏 ⊆ ( 𝑎 ∩ 𝑥 ) ∧ 𝑏 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑏 ( 𝑏 ∩ 𝑦 ) = ∅ )    )
27 onfrALTlem5 ⊢ ( [ ( 𝑎 ∩ 𝑥 ) / 𝑏 ] ( ( 𝑏 ⊆ ( 𝑎 ∩ 𝑥 ) ∧ 𝑏 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑏 ( 𝑏 ∩ 𝑦 ) = ∅ ) ↔ ( ( ( 𝑎 ∩ 𝑥 ) ⊆ ( 𝑎 ∩ 𝑥 ) ∧ ( 𝑎 ∩ 𝑥 ) ≠ ∅ ) → ∃ 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ ) )
28 26 27 e2bi ⊢ (    ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ )    ,    ( 𝑥 ∈ 𝑎 ∧ ¬ ( 𝑎 ∩ 𝑥 ) = ∅ )    ▶    ( ( ( 𝑎 ∩ 𝑥 ) ⊆ ( 𝑎 ∩ 𝑥 ) ∧ ( 𝑎 ∩ 𝑥 ) ≠ ∅ ) → ∃ 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ )    )
29 ssid ⊢ ( 𝑎 ∩ 𝑥 ) ⊆ ( 𝑎 ∩ 𝑥 )
30 simpr ⊢ ( ( 𝑥 ∈ 𝑎 ∧ ¬ ( 𝑎 ∩ 𝑥 ) = ∅ ) → ¬ ( 𝑎 ∩ 𝑥 ) = ∅ )
31 4 30 e2 ⊢ (    ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ )    ,    ( 𝑥 ∈ 𝑎 ∧ ¬ ( 𝑎 ∩ 𝑥 ) = ∅ )    ▶    ¬ ( 𝑎 ∩ 𝑥 ) = ∅    )
32 df-ne ⊢ ( ( 𝑎 ∩ 𝑥 ) ≠ ∅ ↔ ¬ ( 𝑎 ∩ 𝑥 ) = ∅ )
33 32 biimpri ⊢ ( ¬ ( 𝑎 ∩ 𝑥 ) = ∅ → ( 𝑎 ∩ 𝑥 ) ≠ ∅ )
34 31 33 e2 ⊢ (    ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ )    ,    ( 𝑥 ∈ 𝑎 ∧ ¬ ( 𝑎 ∩ 𝑥 ) = ∅ )    ▶    ( 𝑎 ∩ 𝑥 ) ≠ ∅    )
35 pm3.2 ⊢ ( ( 𝑎 ∩ 𝑥 ) ⊆ ( 𝑎 ∩ 𝑥 ) → ( ( 𝑎 ∩ 𝑥 ) ≠ ∅ → ( ( 𝑎 ∩ 𝑥 ) ⊆ ( 𝑎 ∩ 𝑥 ) ∧ ( 𝑎 ∩ 𝑥 ) ≠ ∅ ) ) )
36 29 34 35 e02 ⊢ (    ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ )    ,    ( 𝑥 ∈ 𝑎 ∧ ¬ ( 𝑎 ∩ 𝑥 ) = ∅ )    ▶    ( ( 𝑎 ∩ 𝑥 ) ⊆ ( 𝑎 ∩ 𝑥 ) ∧ ( 𝑎 ∩ 𝑥 ) ≠ ∅ )    )
37 id ⊢ ( ( ( ( 𝑎 ∩ 𝑥 ) ⊆ ( 𝑎 ∩ 𝑥 ) ∧ ( 𝑎 ∩ 𝑥 ) ≠ ∅ ) → ∃ 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ ) → ( ( ( 𝑎 ∩ 𝑥 ) ⊆ ( 𝑎 ∩ 𝑥 ) ∧ ( 𝑎 ∩ 𝑥 ) ≠ ∅ ) → ∃ 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ ) )
38 28 36 37 e22 ⊢ (    ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ )    ,    ( 𝑥 ∈ 𝑎 ∧ ¬ ( 𝑎 ∩ 𝑥 ) = ∅ )    ▶    ∃ 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅    )