Metamath Proof Explorer


Theorem inf3lem3

Description: Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 for detailed description. In the proof, we invoke the Axiom of Regularity in the form of zfreg . (Contributed by NM, 29-Oct-1996)

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

Proof

Step Hyp Ref Expression
1 inf3lem.1 𝐺 = ( 𝑦 ∈ V ↦ { 𝑤𝑥 ∣ ( 𝑤𝑥 ) ⊆ 𝑦 } )
2 inf3lem.2 𝐹 = ( rec ( 𝐺 , ∅ ) ↾ ω )
3 inf3lem.3 𝐴 ∈ V
4 inf3lem.4 𝐵 ∈ V
5 1 2 3 4 inf3lemd ( 𝐴 ∈ ω → ( 𝐹𝐴 ) ⊆ 𝑥 )
6 1 2 3 4 inf3lem2 ( ( 𝑥 ≠ ∅ ∧ 𝑥 𝑥 ) → ( 𝐴 ∈ ω → ( 𝐹𝐴 ) ≠ 𝑥 ) )
7 6 com12 ( 𝐴 ∈ ω → ( ( 𝑥 ≠ ∅ ∧ 𝑥 𝑥 ) → ( 𝐹𝐴 ) ≠ 𝑥 ) )
8 pssdifn0 ( ( ( 𝐹𝐴 ) ⊆ 𝑥 ∧ ( 𝐹𝐴 ) ≠ 𝑥 ) → ( 𝑥 ∖ ( 𝐹𝐴 ) ) ≠ ∅ )
9 5 7 8 syl6an ( 𝐴 ∈ ω → ( ( 𝑥 ≠ ∅ ∧ 𝑥 𝑥 ) → ( 𝑥 ∖ ( 𝐹𝐴 ) ) ≠ ∅ ) )
10 vex 𝑥 ∈ V
11 10 difexi ( 𝑥 ∖ ( 𝐹𝐴 ) ) ∈ V
12 zfreg ( ( ( 𝑥 ∖ ( 𝐹𝐴 ) ) ∈ V ∧ ( 𝑥 ∖ ( 𝐹𝐴 ) ) ≠ ∅ ) → ∃ 𝑣 ∈ ( 𝑥 ∖ ( 𝐹𝐴 ) ) ( 𝑣 ∩ ( 𝑥 ∖ ( 𝐹𝐴 ) ) ) = ∅ )
13 11 12 mpan ( ( 𝑥 ∖ ( 𝐹𝐴 ) ) ≠ ∅ → ∃ 𝑣 ∈ ( 𝑥 ∖ ( 𝐹𝐴 ) ) ( 𝑣 ∩ ( 𝑥 ∖ ( 𝐹𝐴 ) ) ) = ∅ )
14 eldifi ( 𝑣 ∈ ( 𝑥 ∖ ( 𝐹𝐴 ) ) → 𝑣𝑥 )
15 inssdif0 ( ( 𝑣𝑥 ) ⊆ ( 𝐹𝐴 ) ↔ ( 𝑣 ∩ ( 𝑥 ∖ ( 𝐹𝐴 ) ) ) = ∅ )
16 15 biimpri ( ( 𝑣 ∩ ( 𝑥 ∖ ( 𝐹𝐴 ) ) ) = ∅ → ( 𝑣𝑥 ) ⊆ ( 𝐹𝐴 ) )
17 14 16 anim12i ( ( 𝑣 ∈ ( 𝑥 ∖ ( 𝐹𝐴 ) ) ∧ ( 𝑣 ∩ ( 𝑥 ∖ ( 𝐹𝐴 ) ) ) = ∅ ) → ( 𝑣𝑥 ∧ ( 𝑣𝑥 ) ⊆ ( 𝐹𝐴 ) ) )
18 vex 𝑣 ∈ V
19 fvex ( 𝐹𝐴 ) ∈ V
20 1 2 18 19 inf3lema ( 𝑣 ∈ ( 𝐺 ‘ ( 𝐹𝐴 ) ) ↔ ( 𝑣𝑥 ∧ ( 𝑣𝑥 ) ⊆ ( 𝐹𝐴 ) ) )
21 17 20 sylibr ( ( 𝑣 ∈ ( 𝑥 ∖ ( 𝐹𝐴 ) ) ∧ ( 𝑣 ∩ ( 𝑥 ∖ ( 𝐹𝐴 ) ) ) = ∅ ) → 𝑣 ∈ ( 𝐺 ‘ ( 𝐹𝐴 ) ) )
22 1 2 3 4 inf3lemc ( 𝐴 ∈ ω → ( 𝐹 ‘ suc 𝐴 ) = ( 𝐺 ‘ ( 𝐹𝐴 ) ) )
23 22 eleq2d ( 𝐴 ∈ ω → ( 𝑣 ∈ ( 𝐹 ‘ suc 𝐴 ) ↔ 𝑣 ∈ ( 𝐺 ‘ ( 𝐹𝐴 ) ) ) )
24 21 23 syl5ibr ( 𝐴 ∈ ω → ( ( 𝑣 ∈ ( 𝑥 ∖ ( 𝐹𝐴 ) ) ∧ ( 𝑣 ∩ ( 𝑥 ∖ ( 𝐹𝐴 ) ) ) = ∅ ) → 𝑣 ∈ ( 𝐹 ‘ suc 𝐴 ) ) )
25 eldifn ( 𝑣 ∈ ( 𝑥 ∖ ( 𝐹𝐴 ) ) → ¬ 𝑣 ∈ ( 𝐹𝐴 ) )
26 25 adantr ( ( 𝑣 ∈ ( 𝑥 ∖ ( 𝐹𝐴 ) ) ∧ ( 𝑣 ∩ ( 𝑥 ∖ ( 𝐹𝐴 ) ) ) = ∅ ) → ¬ 𝑣 ∈ ( 𝐹𝐴 ) )
27 24 26 jca2 ( 𝐴 ∈ ω → ( ( 𝑣 ∈ ( 𝑥 ∖ ( 𝐹𝐴 ) ) ∧ ( 𝑣 ∩ ( 𝑥 ∖ ( 𝐹𝐴 ) ) ) = ∅ ) → ( 𝑣 ∈ ( 𝐹 ‘ suc 𝐴 ) ∧ ¬ 𝑣 ∈ ( 𝐹𝐴 ) ) ) )
28 eleq2 ( ( 𝐹𝐴 ) = ( 𝐹 ‘ suc 𝐴 ) → ( 𝑣 ∈ ( 𝐹𝐴 ) ↔ 𝑣 ∈ ( 𝐹 ‘ suc 𝐴 ) ) )
29 28 biimprd ( ( 𝐹𝐴 ) = ( 𝐹 ‘ suc 𝐴 ) → ( 𝑣 ∈ ( 𝐹 ‘ suc 𝐴 ) → 𝑣 ∈ ( 𝐹𝐴 ) ) )
30 iman ( ( 𝑣 ∈ ( 𝐹 ‘ suc 𝐴 ) → 𝑣 ∈ ( 𝐹𝐴 ) ) ↔ ¬ ( 𝑣 ∈ ( 𝐹 ‘ suc 𝐴 ) ∧ ¬ 𝑣 ∈ ( 𝐹𝐴 ) ) )
31 29 30 sylib ( ( 𝐹𝐴 ) = ( 𝐹 ‘ suc 𝐴 ) → ¬ ( 𝑣 ∈ ( 𝐹 ‘ suc 𝐴 ) ∧ ¬ 𝑣 ∈ ( 𝐹𝐴 ) ) )
32 31 necon2ai ( ( 𝑣 ∈ ( 𝐹 ‘ suc 𝐴 ) ∧ ¬ 𝑣 ∈ ( 𝐹𝐴 ) ) → ( 𝐹𝐴 ) ≠ ( 𝐹 ‘ suc 𝐴 ) )
33 27 32 syl6 ( 𝐴 ∈ ω → ( ( 𝑣 ∈ ( 𝑥 ∖ ( 𝐹𝐴 ) ) ∧ ( 𝑣 ∩ ( 𝑥 ∖ ( 𝐹𝐴 ) ) ) = ∅ ) → ( 𝐹𝐴 ) ≠ ( 𝐹 ‘ suc 𝐴 ) ) )
34 33 expd ( 𝐴 ∈ ω → ( 𝑣 ∈ ( 𝑥 ∖ ( 𝐹𝐴 ) ) → ( ( 𝑣 ∩ ( 𝑥 ∖ ( 𝐹𝐴 ) ) ) = ∅ → ( 𝐹𝐴 ) ≠ ( 𝐹 ‘ suc 𝐴 ) ) ) )
35 34 rexlimdv ( 𝐴 ∈ ω → ( ∃ 𝑣 ∈ ( 𝑥 ∖ ( 𝐹𝐴 ) ) ( 𝑣 ∩ ( 𝑥 ∖ ( 𝐹𝐴 ) ) ) = ∅ → ( 𝐹𝐴 ) ≠ ( 𝐹 ‘ suc 𝐴 ) ) )
36 13 35 syl5 ( 𝐴 ∈ ω → ( ( 𝑥 ∖ ( 𝐹𝐴 ) ) ≠ ∅ → ( 𝐹𝐴 ) ≠ ( 𝐹 ‘ suc 𝐴 ) ) )
37 9 36 syldc ( ( 𝑥 ≠ ∅ ∧ 𝑥 𝑥 ) → ( 𝐴 ∈ ω → ( 𝐹𝐴 ) ≠ ( 𝐹 ‘ suc 𝐴 ) ) )