Metamath Proof Explorer

Theorem onfrALTlem2

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

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

Proof

Step Hyp Ref Expression
1 simpr ⊢ ( ( ( 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ∧ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ ) ∧ 𝑧 ∈ ( 𝑎 ∩ 𝑦 ) ) → 𝑧 ∈ ( 𝑎 ∩ 𝑦 ) )
2 1 2a1i ⊢ ( ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ ) → ( ( 𝑥 ∈ 𝑎 ∧ ¬ ( 𝑎 ∩ 𝑥 ) = ∅ ) → ( ( ( 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ∧ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ ) ∧ 𝑧 ∈ ( 𝑎 ∩ 𝑦 ) ) → 𝑧 ∈ ( 𝑎 ∩ 𝑦 ) ) ) )
3 inss2 ⊢ ( 𝑎 ∩ 𝑦 ) ⊆ 𝑦
4 3 sseli ⊢ ( 𝑧 ∈ ( 𝑎 ∩ 𝑦 ) → 𝑧 ∈ 𝑦 )
5 2 4 syl8 ⊢ ( ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ ) → ( ( 𝑥 ∈ 𝑎 ∧ ¬ ( 𝑎 ∩ 𝑥 ) = ∅ ) → ( ( ( 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ∧ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ ) ∧ 𝑧 ∈ ( 𝑎 ∩ 𝑦 ) ) → 𝑧 ∈ 𝑦 ) ) )
6 inss1 ⊢ ( 𝑎 ∩ 𝑦 ) ⊆ 𝑎
7 6 sseli ⊢ ( 𝑧 ∈ ( 𝑎 ∩ 𝑦 ) → 𝑧 ∈ 𝑎 )
8 2 7 syl8 ⊢ ( ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ ) → ( ( 𝑥 ∈ 𝑎 ∧ ¬ ( 𝑎 ∩ 𝑥 ) = ∅ ) → ( ( ( 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ∧ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ ) ∧ 𝑧 ∈ ( 𝑎 ∩ 𝑦 ) ) → 𝑧 ∈ 𝑎 ) ) )
9 simpl ⊢ ( ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ ) → 𝑎 ⊆ On )
10 simpl ⊢ ( ( 𝑥 ∈ 𝑎 ∧ ¬ ( 𝑎 ∩ 𝑥 ) = ∅ ) → 𝑥 ∈ 𝑎 )
11 ssel ⊢ ( 𝑎 ⊆ On → ( 𝑥 ∈ 𝑎 → 𝑥 ∈ On ) )
12 9 10 11 syl2im ⊢ ( ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ ) → ( ( 𝑥 ∈ 𝑎 ∧ ¬ ( 𝑎 ∩ 𝑥 ) = ∅ ) → 𝑥 ∈ On ) )
13 eloni ⊢ ( 𝑥 ∈ On → Ord 𝑥 )
14 12 13 syl6 ⊢ ( ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ ) → ( ( 𝑥 ∈ 𝑎 ∧ ¬ ( 𝑎 ∩ 𝑥 ) = ∅ ) → Ord 𝑥 ) )
15 ordtr ⊢ ( Ord 𝑥 → Tr 𝑥 )
16 14 15 syl6 ⊢ ( ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ ) → ( ( 𝑥 ∈ 𝑎 ∧ ¬ ( 𝑎 ∩ 𝑥 ) = ∅ ) → Tr 𝑥 ) )
17 simpll ⊢ ( ( ( 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ∧ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ ) ∧ 𝑧 ∈ ( 𝑎 ∩ 𝑦 ) ) → 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) )
18 17 2a1i ⊢ ( ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ ) → ( ( 𝑥 ∈ 𝑎 ∧ ¬ ( 𝑎 ∩ 𝑥 ) = ∅ ) → ( ( ( 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ∧ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ ) ∧ 𝑧 ∈ ( 𝑎 ∩ 𝑦 ) ) → 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ) ) )
19 inss2 ⊢ ( 𝑎 ∩ 𝑥 ) ⊆ 𝑥
20 19 sseli ⊢ ( 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) → 𝑦 ∈ 𝑥 )
21 18 20 syl8 ⊢ ( ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ ) → ( ( 𝑥 ∈ 𝑎 ∧ ¬ ( 𝑎 ∩ 𝑥 ) = ∅ ) → ( ( ( 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ∧ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ ) ∧ 𝑧 ∈ ( 𝑎 ∩ 𝑦 ) ) → 𝑦 ∈ 𝑥 ) ) )
22 trel ⊢ ( Tr 𝑥 → ( ( 𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 ) )
23 22 expcomd ⊢ ( Tr 𝑥 → ( 𝑦 ∈ 𝑥 → ( 𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥 ) ) )
24 16 21 5 23 ee233 ⊢ ( ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ ) → ( ( 𝑥 ∈ 𝑎 ∧ ¬ ( 𝑎 ∩ 𝑥 ) = ∅ ) → ( ( ( 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ∧ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ ) ∧ 𝑧 ∈ ( 𝑎 ∩ 𝑦 ) ) → 𝑧 ∈ 𝑥 ) ) )
25 elin ⊢ ( 𝑧 ∈ ( 𝑎 ∩ 𝑥 ) ↔ ( 𝑧 ∈ 𝑎 ∧ 𝑧 ∈ 𝑥 ) )
26 25 simplbi2 ⊢ ( 𝑧 ∈ 𝑎 → ( 𝑧 ∈ 𝑥 → 𝑧 ∈ ( 𝑎 ∩ 𝑥 ) ) )
27 8 24 26 ee33 ⊢ ( ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ ) → ( ( 𝑥 ∈ 𝑎 ∧ ¬ ( 𝑎 ∩ 𝑥 ) = ∅ ) → ( ( ( 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ∧ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ ) ∧ 𝑧 ∈ ( 𝑎 ∩ 𝑦 ) ) → 𝑧 ∈ ( 𝑎 ∩ 𝑥 ) ) ) )
28 elin ⊢ ( 𝑧 ∈ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) ↔ ( 𝑧 ∈ ( 𝑎 ∩ 𝑥 ) ∧ 𝑧 ∈ 𝑦 ) )
29 28 simplbi2com ⊢ ( 𝑧 ∈ 𝑦 → ( 𝑧 ∈ ( 𝑎 ∩ 𝑥 ) → 𝑧 ∈ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) ) )
30 5 27 29 ee33 ⊢ ( ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ ) → ( ( 𝑥 ∈ 𝑎 ∧ ¬ ( 𝑎 ∩ 𝑥 ) = ∅ ) → ( ( ( 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ∧ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ ) ∧ 𝑧 ∈ ( 𝑎 ∩ 𝑦 ) ) → 𝑧 ∈ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) ) ) )
31 30 exp4a ⊢ ( ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ ) → ( ( 𝑥 ∈ 𝑎 ∧ ¬ ( 𝑎 ∩ 𝑥 ) = ∅ ) → ( ( 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ∧ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ ) → ( 𝑧 ∈ ( 𝑎 ∩ 𝑦 ) → 𝑧 ∈ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) ) ) ) )
32 31 ggen31 ⊢ ( ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ ) → ( ( 𝑥 ∈ 𝑎 ∧ ¬ ( 𝑎 ∩ 𝑥 ) = ∅ ) → ( ( 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ∧ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ ) → ∀ 𝑧 ( 𝑧 ∈ ( 𝑎 ∩ 𝑦 ) → 𝑧 ∈ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) ) ) ) )
33 df-ss ⊢ ( ( 𝑎 ∩ 𝑦 ) ⊆ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) ↔ ∀ 𝑧 ( 𝑧 ∈ ( 𝑎 ∩ 𝑦 ) → 𝑧 ∈ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) ) )
34 33 biimpri ⊢ ( ∀ 𝑧 ( 𝑧 ∈ ( 𝑎 ∩ 𝑦 ) → 𝑧 ∈ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) ) → ( 𝑎 ∩ 𝑦 ) ⊆ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) )
35 32 34 syl8 ⊢ ( ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ ) → ( ( 𝑥 ∈ 𝑎 ∧ ¬ ( 𝑎 ∩ 𝑥 ) = ∅ ) → ( ( 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ∧ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ ) → ( 𝑎 ∩ 𝑦 ) ⊆ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) ) ) )
36 simpr ⊢ ( ( 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ∧ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ ) → ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ )
37 36 2a1i ⊢ ( ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ ) → ( ( 𝑥 ∈ 𝑎 ∧ ¬ ( 𝑎 ∩ 𝑥 ) = ∅ ) → ( ( 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ∧ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ ) → ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ ) ) )
38 sseq0 ⊢ ( ( ( 𝑎 ∩ 𝑦 ) ⊆ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) ∧ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ ) → ( 𝑎 ∩ 𝑦 ) = ∅ )
39 38 ex ⊢ ( ( 𝑎 ∩ 𝑦 ) ⊆ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) → ( ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ → ( 𝑎 ∩ 𝑦 ) = ∅ ) )
40 35 37 39 ee33 ⊢ ( ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ ) → ( ( 𝑥 ∈ 𝑎 ∧ ¬ ( 𝑎 ∩ 𝑥 ) = ∅ ) → ( ( 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ∧ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ ) → ( 𝑎 ∩ 𝑦 ) = ∅ ) ) )
41 simpl ⊢ ( ( 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ∧ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ ) → 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) )
42 41 2a1i ⊢ ( ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ ) → ( ( 𝑥 ∈ 𝑎 ∧ ¬ ( 𝑎 ∩ 𝑥 ) = ∅ ) → ( ( 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ∧ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ ) → 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ) ) )
43 inss1 ⊢ ( 𝑎 ∩ 𝑥 ) ⊆ 𝑎
44 43 sseli ⊢ ( 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) → 𝑦 ∈ 𝑎 )
45 42 44 syl8 ⊢ ( ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ ) → ( ( 𝑥 ∈ 𝑎 ∧ ¬ ( 𝑎 ∩ 𝑥 ) = ∅ ) → ( ( 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ∧ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ ) → 𝑦 ∈ 𝑎 ) ) )
46 pm3.21 ⊢ ( ( 𝑎 ∩ 𝑦 ) = ∅ → ( 𝑦 ∈ 𝑎 → ( 𝑦 ∈ 𝑎 ∧ ( 𝑎 ∩ 𝑦 ) = ∅ ) ) )
47 40 45 46 ee33 ⊢ ( ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ ) → ( ( 𝑥 ∈ 𝑎 ∧ ¬ ( 𝑎 ∩ 𝑥 ) = ∅ ) → ( ( 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ∧ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ ) → ( 𝑦 ∈ 𝑎 ∧ ( 𝑎 ∩ 𝑦 ) = ∅ ) ) ) )
48 47 alrimdv ⊢ ( ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ ) → ( ( 𝑥 ∈ 𝑎 ∧ ¬ ( 𝑎 ∩ 𝑥 ) = ∅ ) → ∀ 𝑦 ( ( 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ∧ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ ) → ( 𝑦 ∈ 𝑎 ∧ ( 𝑎 ∩ 𝑦 ) = ∅ ) ) ) )
49 onfrALTlem3 ⊢ ( ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ ) → ( ( 𝑥 ∈ 𝑎 ∧ ¬ ( 𝑎 ∩ 𝑥 ) = ∅ ) → ∃ 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ ) )
50 df-rex ⊢ ( ∃ 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ ↔ ∃ 𝑦 ( 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ∧ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ ) )
51 49 50 imbitrdi ⊢ ( ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ ) → ( ( 𝑥 ∈ 𝑎 ∧ ¬ ( 𝑎 ∩ 𝑥 ) = ∅ ) → ∃ 𝑦 ( 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ∧ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ ) ) )
52 exim ⊢ ( ∀ 𝑦 ( ( 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ∧ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ ) → ( 𝑦 ∈ 𝑎 ∧ ( 𝑎 ∩ 𝑦 ) = ∅ ) ) → ( ∃ 𝑦 ( 𝑦 ∈ ( 𝑎 ∩ 𝑥 ) ∧ ( ( 𝑎 ∩ 𝑥 ) ∩ 𝑦 ) = ∅ ) → ∃ 𝑦 ( 𝑦 ∈ 𝑎 ∧ ( 𝑎 ∩ 𝑦 ) = ∅ ) ) )
53 48 51 52 syl6c ⊢ ( ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ ) → ( ( 𝑥 ∈ 𝑎 ∧ ¬ ( 𝑎 ∩ 𝑥 ) = ∅ ) → ∃ 𝑦 ( 𝑦 ∈ 𝑎 ∧ ( 𝑎 ∩ 𝑦 ) = ∅ ) ) )
54 df-rex ⊢ ( ∃ 𝑦 ∈ 𝑎 ( 𝑎 ∩ 𝑦 ) = ∅ ↔ ∃ 𝑦 ( 𝑦 ∈ 𝑎 ∧ ( 𝑎 ∩ 𝑦 ) = ∅ ) )
55 53 54 imbitrrdi ⊢ ( ( 𝑎 ⊆ On ∧ 𝑎 ≠ ∅ ) → ( ( 𝑥 ∈ 𝑎 ∧ ¬ ( 𝑎 ∩ 𝑥 ) = ∅ ) → ∃ 𝑦 ∈ 𝑎 ( 𝑎 ∩ 𝑦 ) = ∅ ) )