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

Metamath Proof Explorer

Theorem inf3lem2

Description: Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 for detailed description. (Contributed by NM, 28-Oct-1996)

Ref Expression
Hypotheses inf3lem.1 ⊢ 𝐺 = ( 𝑦 ∈ V ↦ { 𝑤 ∈ 𝑥 ∣ ( 𝑤 ∩ 𝑥 ) ⊆ 𝑦 } )
inf3lem.2 ⊢ 𝐹 = ( rec ( 𝐺 , ∅ ) ↾ ω )
inf3lem.3 ⊢ 𝐴 ∈ V
inf3lem.4 ⊢ 𝐵 ∈ V
Assertion inf3lem2 ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) → ( 𝐴 ∈ ω → ( 𝐹 ‘ 𝐴 ) ≠ 𝑥 ) )

Proof

Step Hyp Ref Expression
1 inf3lem.1 ⊢ 𝐺 = ( 𝑦 ∈ V ↦ { 𝑤 ∈ 𝑥 ∣ ( 𝑤 ∩ 𝑥 ) ⊆ 𝑦 } )
2 inf3lem.2 ⊢ 𝐹 = ( rec ( 𝐺 , ∅ ) ↾ ω )
3 inf3lem.3 ⊢ 𝐴 ∈ V
4 inf3lem.4 ⊢ 𝐵 ∈ V
5 fveq2 ⊢ ( 𝑣 = ∅ → ( 𝐹 ‘ 𝑣 ) = ( 𝐹 ‘ ∅ ) )
6 5 neeq1d ⊢ ( 𝑣 = ∅ → ( ( 𝐹 ‘ 𝑣 ) ≠ 𝑥 ↔ ( 𝐹 ‘ ∅ ) ≠ 𝑥 ) )
7 6 imbi2d ⊢ ( 𝑣 = ∅ → ( ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) → ( 𝐹 ‘ 𝑣 ) ≠ 𝑥 ) ↔ ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) → ( 𝐹 ‘ ∅ ) ≠ 𝑥 ) ) )
8 fveq2 ⊢ ( 𝑣 = 𝑢 → ( 𝐹 ‘ 𝑣 ) = ( 𝐹 ‘ 𝑢 ) )
9 8 neeq1d ⊢ ( 𝑣 = 𝑢 → ( ( 𝐹 ‘ 𝑣 ) ≠ 𝑥 ↔ ( 𝐹 ‘ 𝑢 ) ≠ 𝑥 ) )
10 9 imbi2d ⊢ ( 𝑣 = 𝑢 → ( ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) → ( 𝐹 ‘ 𝑣 ) ≠ 𝑥 ) ↔ ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) → ( 𝐹 ‘ 𝑢 ) ≠ 𝑥 ) ) )
11 fveq2 ⊢ ( 𝑣 = suc 𝑢 → ( 𝐹 ‘ 𝑣 ) = ( 𝐹 ‘ suc 𝑢 ) )
12 11 neeq1d ⊢ ( 𝑣 = suc 𝑢 → ( ( 𝐹 ‘ 𝑣 ) ≠ 𝑥 ↔ ( 𝐹 ‘ suc 𝑢 ) ≠ 𝑥 ) )
13 12 imbi2d ⊢ ( 𝑣 = suc 𝑢 → ( ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) → ( 𝐹 ‘ 𝑣 ) ≠ 𝑥 ) ↔ ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) → ( 𝐹 ‘ suc 𝑢 ) ≠ 𝑥 ) ) )
14 fveq2 ⊢ ( 𝑣 = 𝐴 → ( 𝐹 ‘ 𝑣 ) = ( 𝐹 ‘ 𝐴 ) )
15 14 neeq1d ⊢ ( 𝑣 = 𝐴 → ( ( 𝐹 ‘ 𝑣 ) ≠ 𝑥 ↔ ( 𝐹 ‘ 𝐴 ) ≠ 𝑥 ) )
16 15 imbi2d ⊢ ( 𝑣 = 𝐴 → ( ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) → ( 𝐹 ‘ 𝑣 ) ≠ 𝑥 ) ↔ ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) → ( 𝐹 ‘ 𝐴 ) ≠ 𝑥 ) ) )
17 1 2 3 4 inf3lemb ⊢ ( 𝐹 ‘ ∅ ) = ∅
18 17 eqeq1i ⊢ ( ( 𝐹 ‘ ∅ ) = 𝑥 ↔ ∅ = 𝑥 )
19 eqcom ⊢ ( ∅ = 𝑥 ↔ 𝑥 = ∅ )
20 18 19 sylbb ⊢ ( ( 𝐹 ‘ ∅ ) = 𝑥 → 𝑥 = ∅ )
21 20 necon3i ⊢ ( 𝑥 ≠ ∅ → ( 𝐹 ‘ ∅ ) ≠ 𝑥 )
22 21 adantr ⊢ ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) → ( 𝐹 ‘ ∅ ) ≠ 𝑥 )
23 vex ⊢ 𝑢 ∈ V
24 1 2 23 4 inf3lemd ⊢ ( 𝑢 ∈ ω → ( 𝐹 ‘ 𝑢 ) ⊆ 𝑥 )
25 df-pss ⊢ ( ( 𝐹 ‘ 𝑢 ) ⊊ 𝑥 ↔ ( ( 𝐹 ‘ 𝑢 ) ⊆ 𝑥 ∧ ( 𝐹 ‘ 𝑢 ) ≠ 𝑥 ) )
26 pssnel ⊢ ( ( 𝐹 ‘ 𝑢 ) ⊊ 𝑥 → ∃ 𝑣 ( 𝑣 ∈ 𝑥 ∧ ¬ 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) ) )
27 25 26 sylbir ⊢ ( ( ( 𝐹 ‘ 𝑢 ) ⊆ 𝑥 ∧ ( 𝐹 ‘ 𝑢 ) ≠ 𝑥 ) → ∃ 𝑣 ( 𝑣 ∈ 𝑥 ∧ ¬ 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) ) )
28 ssel ⊢ ( 𝑥 ⊆ ∪ 𝑥 → ( 𝑣 ∈ 𝑥 → 𝑣 ∈ ∪ 𝑥 ) )
29 eluni ⊢ ( 𝑣 ∈ ∪ 𝑥 ↔ ∃ 𝑓 ( 𝑣 ∈ 𝑓 ∧ 𝑓 ∈ 𝑥 ) )
30 28 29 imbitrdi ⊢ ( 𝑥 ⊆ ∪ 𝑥 → ( 𝑣 ∈ 𝑥 → ∃ 𝑓 ( 𝑣 ∈ 𝑓 ∧ 𝑓 ∈ 𝑥 ) ) )
31 eleq2 ⊢ ( ( 𝐹 ‘ suc 𝑢 ) = 𝑥 → ( 𝑓 ∈ ( 𝐹 ‘ suc 𝑢 ) ↔ 𝑓 ∈ 𝑥 ) )
32 31 biimparc ⊢ ( ( 𝑓 ∈ 𝑥 ∧ ( 𝐹 ‘ suc 𝑢 ) = 𝑥 ) → 𝑓 ∈ ( 𝐹 ‘ suc 𝑢 ) )
33 1 2 23 4 inf3lemc ⊢ ( 𝑢 ∈ ω → ( 𝐹 ‘ suc 𝑢 ) = ( 𝐺 ‘ ( 𝐹 ‘ 𝑢 ) ) )
34 33 eleq2d ⊢ ( 𝑢 ∈ ω → ( 𝑓 ∈ ( 𝐹 ‘ suc 𝑢 ) ↔ 𝑓 ∈ ( 𝐺 ‘ ( 𝐹 ‘ 𝑢 ) ) ) )
35 elin ⊢ ( 𝑣 ∈ ( 𝑓 ∩ 𝑥 ) ↔ ( 𝑣 ∈ 𝑓 ∧ 𝑣 ∈ 𝑥 ) )
36 vex ⊢ 𝑓 ∈ V
37 fvex ⊢ ( 𝐹 ‘ 𝑢 ) ∈ V
38 1 2 36 37 inf3lema ⊢ ( 𝑓 ∈ ( 𝐺 ‘ ( 𝐹 ‘ 𝑢 ) ) ↔ ( 𝑓 ∈ 𝑥 ∧ ( 𝑓 ∩ 𝑥 ) ⊆ ( 𝐹 ‘ 𝑢 ) ) )
39 38 simprbi ⊢ ( 𝑓 ∈ ( 𝐺 ‘ ( 𝐹 ‘ 𝑢 ) ) → ( 𝑓 ∩ 𝑥 ) ⊆ ( 𝐹 ‘ 𝑢 ) )
40 39 sseld ⊢ ( 𝑓 ∈ ( 𝐺 ‘ ( 𝐹 ‘ 𝑢 ) ) → ( 𝑣 ∈ ( 𝑓 ∩ 𝑥 ) → 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) ) )
41 35 40 biimtrrid ⊢ ( 𝑓 ∈ ( 𝐺 ‘ ( 𝐹 ‘ 𝑢 ) ) → ( ( 𝑣 ∈ 𝑓 ∧ 𝑣 ∈ 𝑥 ) → 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) ) )
42 34 41 biimtrdi ⊢ ( 𝑢 ∈ ω → ( 𝑓 ∈ ( 𝐹 ‘ suc 𝑢 ) → ( ( 𝑣 ∈ 𝑓 ∧ 𝑣 ∈ 𝑥 ) → 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) ) ) )
43 32 42 syl5 ⊢ ( 𝑢 ∈ ω → ( ( 𝑓 ∈ 𝑥 ∧ ( 𝐹 ‘ suc 𝑢 ) = 𝑥 ) → ( ( 𝑣 ∈ 𝑓 ∧ 𝑣 ∈ 𝑥 ) → 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) ) ) )
44 43 com23 ⊢ ( 𝑢 ∈ ω → ( ( 𝑣 ∈ 𝑓 ∧ 𝑣 ∈ 𝑥 ) → ( ( 𝑓 ∈ 𝑥 ∧ ( 𝐹 ‘ suc 𝑢 ) = 𝑥 ) → 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) ) ) )
45 44 exp5c ⊢ ( 𝑢 ∈ ω → ( 𝑣 ∈ 𝑓 → ( 𝑣 ∈ 𝑥 → ( 𝑓 ∈ 𝑥 → ( ( 𝐹 ‘ suc 𝑢 ) = 𝑥 → 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) ) ) ) ) )
46 45 com34 ⊢ ( 𝑢 ∈ ω → ( 𝑣 ∈ 𝑓 → ( 𝑓 ∈ 𝑥 → ( 𝑣 ∈ 𝑥 → ( ( 𝐹 ‘ suc 𝑢 ) = 𝑥 → 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) ) ) ) ) )
47 46 impd ⊢ ( 𝑢 ∈ ω → ( ( 𝑣 ∈ 𝑓 ∧ 𝑓 ∈ 𝑥 ) → ( 𝑣 ∈ 𝑥 → ( ( 𝐹 ‘ suc 𝑢 ) = 𝑥 → 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) ) ) ) )
48 47 exlimdv ⊢ ( 𝑢 ∈ ω → ( ∃ 𝑓 ( 𝑣 ∈ 𝑓 ∧ 𝑓 ∈ 𝑥 ) → ( 𝑣 ∈ 𝑥 → ( ( 𝐹 ‘ suc 𝑢 ) = 𝑥 → 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) ) ) ) )
49 30 48 sylan9r ⊢ ( ( 𝑢 ∈ ω ∧ 𝑥 ⊆ ∪ 𝑥 ) → ( 𝑣 ∈ 𝑥 → ( 𝑣 ∈ 𝑥 → ( ( 𝐹 ‘ suc 𝑢 ) = 𝑥 → 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) ) ) ) )
50 49 pm2.43d ⊢ ( ( 𝑢 ∈ ω ∧ 𝑥 ⊆ ∪ 𝑥 ) → ( 𝑣 ∈ 𝑥 → ( ( 𝐹 ‘ suc 𝑢 ) = 𝑥 → 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) ) ) )
51 id ⊢ ( ( ( 𝐹 ‘ suc 𝑢 ) = 𝑥 → 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) ) → ( ( 𝐹 ‘ suc 𝑢 ) = 𝑥 → 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) ) )
52 51 necon3bd ⊢ ( ( ( 𝐹 ‘ suc 𝑢 ) = 𝑥 → 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) ) → ( ¬ 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) → ( 𝐹 ‘ suc 𝑢 ) ≠ 𝑥 ) )
53 50 52 syl6 ⊢ ( ( 𝑢 ∈ ω ∧ 𝑥 ⊆ ∪ 𝑥 ) → ( 𝑣 ∈ 𝑥 → ( ¬ 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) → ( 𝐹 ‘ suc 𝑢 ) ≠ 𝑥 ) ) )
54 53 impd ⊢ ( ( 𝑢 ∈ ω ∧ 𝑥 ⊆ ∪ 𝑥 ) → ( ( 𝑣 ∈ 𝑥 ∧ ¬ 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) ) → ( 𝐹 ‘ suc 𝑢 ) ≠ 𝑥 ) )
55 54 exlimdv ⊢ ( ( 𝑢 ∈ ω ∧ 𝑥 ⊆ ∪ 𝑥 ) → ( ∃ 𝑣 ( 𝑣 ∈ 𝑥 ∧ ¬ 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) ) → ( 𝐹 ‘ suc 𝑢 ) ≠ 𝑥 ) )
56 27 55 syl5 ⊢ ( ( 𝑢 ∈ ω ∧ 𝑥 ⊆ ∪ 𝑥 ) → ( ( ( 𝐹 ‘ 𝑢 ) ⊆ 𝑥 ∧ ( 𝐹 ‘ 𝑢 ) ≠ 𝑥 ) → ( 𝐹 ‘ suc 𝑢 ) ≠ 𝑥 ) )
57 24 56 sylani ⊢ ( ( 𝑢 ∈ ω ∧ 𝑥 ⊆ ∪ 𝑥 ) → ( ( 𝑢 ∈ ω ∧ ( 𝐹 ‘ 𝑢 ) ≠ 𝑥 ) → ( 𝐹 ‘ suc 𝑢 ) ≠ 𝑥 ) )
58 57 exp4b ⊢ ( 𝑢 ∈ ω → ( 𝑥 ⊆ ∪ 𝑥 → ( 𝑢 ∈ ω → ( ( 𝐹 ‘ 𝑢 ) ≠ 𝑥 → ( 𝐹 ‘ suc 𝑢 ) ≠ 𝑥 ) ) ) )
59 58 pm2.43a ⊢ ( 𝑢 ∈ ω → ( 𝑥 ⊆ ∪ 𝑥 → ( ( 𝐹 ‘ 𝑢 ) ≠ 𝑥 → ( 𝐹 ‘ suc 𝑢 ) ≠ 𝑥 ) ) )
60 59 adantld ⊢ ( 𝑢 ∈ ω → ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) → ( ( 𝐹 ‘ 𝑢 ) ≠ 𝑥 → ( 𝐹 ‘ suc 𝑢 ) ≠ 𝑥 ) ) )
61 60 a2d ⊢ ( 𝑢 ∈ ω → ( ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) → ( 𝐹 ‘ 𝑢 ) ≠ 𝑥 ) → ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) → ( 𝐹 ‘ suc 𝑢 ) ≠ 𝑥 ) ) )
62 7 10 13 16 22 61 finds ⊢ ( 𝐴 ∈ ω → ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) → ( 𝐹 ‘ 𝐴 ) ≠ 𝑥 ) )
63 62 com12 ⊢ ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) → ( 𝐴 ∈ ω → ( 𝐹 ‘ 𝐴 ) ≠ 𝑥 ) )