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

Metamath Proof Explorer

Theorem inf3lem5

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

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

Proof

Step Hyp Ref Expression
1 inf3lem.1 ⊢ 𝐺 = ( 𝑦 ∈ V ↦ { 𝑤 ∈ 𝑥 ∣ ( 𝑤 ∩ 𝑥 ) ⊆ 𝑦 } )
2 inf3lem.2 ⊢ 𝐹 = ( rec ( 𝐺 , ∅ ) ↾ ω )
3 inf3lem.3 ⊢ 𝐴 ∈ V
4 inf3lem.4 ⊢ 𝐵 ∈ V
5 elnn ⊢ ( ( 𝐵 ∈ 𝐴 ∧ 𝐴 ∈ ω ) → 𝐵 ∈ ω )
6 5 ancoms ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴 ) → 𝐵 ∈ ω )
7 nnord ⊢ ( 𝐴 ∈ ω → Ord 𝐴 )
8 ordsucss ⊢ ( Ord 𝐴 → ( 𝐵 ∈ 𝐴 → suc 𝐵 ⊆ 𝐴 ) )
9 7 8 syl ⊢ ( 𝐴 ∈ ω → ( 𝐵 ∈ 𝐴 → suc 𝐵 ⊆ 𝐴 ) )
10 9 adantr ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐵 ∈ 𝐴 → suc 𝐵 ⊆ 𝐴 ) )
11 peano2b ⊢ ( 𝐵 ∈ ω ↔ suc 𝐵 ∈ ω )
12 fveq2 ⊢ ( 𝑣 = suc 𝐵 → ( 𝐹 ‘ 𝑣 ) = ( 𝐹 ‘ suc 𝐵 ) )
13 12 psseq2d ⊢ ( 𝑣 = suc 𝐵 → ( ( 𝐹 ‘ 𝐵 ) ⊊ ( 𝐹 ‘ 𝑣 ) ↔ ( 𝐹 ‘ 𝐵 ) ⊊ ( 𝐹 ‘ suc 𝐵 ) ) )
14 13 imbi2d ⊢ ( 𝑣 = suc 𝐵 → ( ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) → ( 𝐹 ‘ 𝐵 ) ⊊ ( 𝐹 ‘ 𝑣 ) ) ↔ ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) → ( 𝐹 ‘ 𝐵 ) ⊊ ( 𝐹 ‘ suc 𝐵 ) ) ) )
15 fveq2 ⊢ ( 𝑣 = 𝑢 → ( 𝐹 ‘ 𝑣 ) = ( 𝐹 ‘ 𝑢 ) )
16 15 psseq2d ⊢ ( 𝑣 = 𝑢 → ( ( 𝐹 ‘ 𝐵 ) ⊊ ( 𝐹 ‘ 𝑣 ) ↔ ( 𝐹 ‘ 𝐵 ) ⊊ ( 𝐹 ‘ 𝑢 ) ) )
17 16 imbi2d ⊢ ( 𝑣 = 𝑢 → ( ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) → ( 𝐹 ‘ 𝐵 ) ⊊ ( 𝐹 ‘ 𝑣 ) ) ↔ ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) → ( 𝐹 ‘ 𝐵 ) ⊊ ( 𝐹 ‘ 𝑢 ) ) ) )
18 fveq2 ⊢ ( 𝑣 = suc 𝑢 → ( 𝐹 ‘ 𝑣 ) = ( 𝐹 ‘ suc 𝑢 ) )
19 18 psseq2d ⊢ ( 𝑣 = suc 𝑢 → ( ( 𝐹 ‘ 𝐵 ) ⊊ ( 𝐹 ‘ 𝑣 ) ↔ ( 𝐹 ‘ 𝐵 ) ⊊ ( 𝐹 ‘ suc 𝑢 ) ) )
20 19 imbi2d ⊢ ( 𝑣 = suc 𝑢 → ( ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) → ( 𝐹 ‘ 𝐵 ) ⊊ ( 𝐹 ‘ 𝑣 ) ) ↔ ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) → ( 𝐹 ‘ 𝐵 ) ⊊ ( 𝐹 ‘ suc 𝑢 ) ) ) )
21 fveq2 ⊢ ( 𝑣 = 𝐴 → ( 𝐹 ‘ 𝑣 ) = ( 𝐹 ‘ 𝐴 ) )
22 21 psseq2d ⊢ ( 𝑣 = 𝐴 → ( ( 𝐹 ‘ 𝐵 ) ⊊ ( 𝐹 ‘ 𝑣 ) ↔ ( 𝐹 ‘ 𝐵 ) ⊊ ( 𝐹 ‘ 𝐴 ) ) )
23 22 imbi2d ⊢ ( 𝑣 = 𝐴 → ( ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) → ( 𝐹 ‘ 𝐵 ) ⊊ ( 𝐹 ‘ 𝑣 ) ) ↔ ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) → ( 𝐹 ‘ 𝐵 ) ⊊ ( 𝐹 ‘ 𝐴 ) ) ) )
24 1 2 4 4 inf3lem4 ⊢ ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) → ( 𝐵 ∈ ω → ( 𝐹 ‘ 𝐵 ) ⊊ ( 𝐹 ‘ suc 𝐵 ) ) )
25 24 com12 ⊢ ( 𝐵 ∈ ω → ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) → ( 𝐹 ‘ 𝐵 ) ⊊ ( 𝐹 ‘ suc 𝐵 ) ) )
26 11 25 sylbir ⊢ ( suc 𝐵 ∈ ω → ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) → ( 𝐹 ‘ 𝐵 ) ⊊ ( 𝐹 ‘ suc 𝐵 ) ) )
27 vex ⊢ 𝑢 ∈ V
28 1 2 27 4 inf3lem4 ⊢ ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) → ( 𝑢 ∈ ω → ( 𝐹 ‘ 𝑢 ) ⊊ ( 𝐹 ‘ suc 𝑢 ) ) )
29 psstr ⊢ ( ( ( 𝐹 ‘ 𝐵 ) ⊊ ( 𝐹 ‘ 𝑢 ) ∧ ( 𝐹 ‘ 𝑢 ) ⊊ ( 𝐹 ‘ suc 𝑢 ) ) → ( 𝐹 ‘ 𝐵 ) ⊊ ( 𝐹 ‘ suc 𝑢 ) )
30 29 expcom ⊢ ( ( 𝐹 ‘ 𝑢 ) ⊊ ( 𝐹 ‘ suc 𝑢 ) → ( ( 𝐹 ‘ 𝐵 ) ⊊ ( 𝐹 ‘ 𝑢 ) → ( 𝐹 ‘ 𝐵 ) ⊊ ( 𝐹 ‘ suc 𝑢 ) ) )
31 28 30 syl6com ⊢ ( 𝑢 ∈ ω → ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) → ( ( 𝐹 ‘ 𝐵 ) ⊊ ( 𝐹 ‘ 𝑢 ) → ( 𝐹 ‘ 𝐵 ) ⊊ ( 𝐹 ‘ suc 𝑢 ) ) ) )
32 31 a2d ⊢ ( 𝑢 ∈ ω → ( ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) → ( 𝐹 ‘ 𝐵 ) ⊊ ( 𝐹 ‘ 𝑢 ) ) → ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) → ( 𝐹 ‘ 𝐵 ) ⊊ ( 𝐹 ‘ suc 𝑢 ) ) ) )
33 32 ad2antrr ⊢ ( ( ( 𝑢 ∈ ω ∧ suc 𝐵 ∈ ω ) ∧ suc 𝐵 ⊆ 𝑢 ) → ( ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) → ( 𝐹 ‘ 𝐵 ) ⊊ ( 𝐹 ‘ 𝑢 ) ) → ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) → ( 𝐹 ‘ 𝐵 ) ⊊ ( 𝐹 ‘ suc 𝑢 ) ) ) )
34 14 17 20 23 26 33 findsg ⊢ ( ( ( 𝐴 ∈ ω ∧ suc 𝐵 ∈ ω ) ∧ suc 𝐵 ⊆ 𝐴 ) → ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) → ( 𝐹 ‘ 𝐵 ) ⊊ ( 𝐹 ‘ 𝐴 ) ) )
35 34 ex ⊢ ( ( 𝐴 ∈ ω ∧ suc 𝐵 ∈ ω ) → ( suc 𝐵 ⊆ 𝐴 → ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) → ( 𝐹 ‘ 𝐵 ) ⊊ ( 𝐹 ‘ 𝐴 ) ) ) )
36 11 35 sylan2b ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( suc 𝐵 ⊆ 𝐴 → ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) → ( 𝐹 ‘ 𝐵 ) ⊊ ( 𝐹 ‘ 𝐴 ) ) ) )
37 10 36 syld ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐵 ∈ 𝐴 → ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) → ( 𝐹 ‘ 𝐵 ) ⊊ ( 𝐹 ‘ 𝐴 ) ) ) )
38 37 impancom ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴 ) → ( 𝐵 ∈ ω → ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) → ( 𝐹 ‘ 𝐵 ) ⊊ ( 𝐹 ‘ 𝐴 ) ) ) )
39 6 38 mpd ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴 ) → ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) → ( 𝐹 ‘ 𝐵 ) ⊊ ( 𝐹 ‘ 𝐴 ) ) )
40 39 com12 ⊢ ( ( 𝑥 ≠ ∅ ∧ 𝑥 ⊆ ∪ 𝑥 ) → ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴 ) → ( 𝐹 ‘ 𝐵 ) ⊊ ( 𝐹 ‘ 𝐴 ) ) )