Theorem bnj601 31871

Description: Technical lemma for bnj852 31872. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)

Hypotheses

Ref	Expression
bnj601.1	⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅))
bnj601.2	⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))
bnj601.3	⊢ 𝐷 = (ω ∖ {∅})
bnj601.4	⊢ (𝜒 ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃!𝑓(𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)))
bnj601.5	⊢ (𝜃 ↔ ∀𝑚 ∈ 𝐷 (𝑚 E 𝑛 → [𝑚 / 𝑛]𝜒))

Assertion

Ref	Expression
bnj601	⊢ (𝑛 ≠ 1o → ((𝑛 ∈ 𝐷 ∧ 𝜃) → 𝜒))

Distinct variable groups:   𝐴,𝑓,𝑖,𝑚,𝑛,𝑦   𝐷,𝑓,𝑖   𝑅,𝑓,𝑖,𝑚,𝑛,𝑦   𝑥,𝑓,𝑚,𝑛   𝜑,𝑖,𝑚   𝜓,𝑚

Allowed substitution hints:   𝜑(𝑥,𝑦,𝑓,𝑛)   𝜓(𝑥,𝑦,𝑓,𝑖,𝑛)   𝜒(𝑥,𝑦,𝑓,𝑖,𝑚,𝑛)   𝜃(𝑥,𝑦,𝑓,𝑖,𝑚,𝑛)   𝐴(𝑥)   𝐷(𝑥,𝑦,𝑚,𝑛)   𝑅(𝑥)

Proof of Theorem bnj601

Dummy variables 𝑝 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		bnj601.1	. 2 ⊢ (𝜑 ↔ (𝑓‘∅) = pred(𝑥, 𝐴, 𝑅))
2		bnj601.2	. 2 ⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))
3		bnj601.3	. 2 ⊢ 𝐷 = (ω ∖ {∅})
4		bnj601.4	. 2 ⊢ (𝜒 ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → ∃!𝑓(𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)))
5		bnj601.5	. 2 ⊢ (𝜃 ↔ ∀𝑚 ∈ 𝐷 (𝑚 E 𝑛 → [𝑚 / 𝑛]𝜒))
6		biid 253	. 2 ⊢ ([𝑚 / 𝑛]𝜑 ↔ [𝑚 / 𝑛]𝜑)
7		biid 253	. 2 ⊢ ([𝑚 / 𝑛]𝜓 ↔ [𝑚 / 𝑛]𝜓)
8		biid 253	. 2 ⊢ ([𝑚 / 𝑛]𝜒 ↔ [𝑚 / 𝑛]𝜒)
9		bnj602 31866	. . . . . . 7 ⊢ (𝑦 = 𝑧 → pred(𝑦, 𝐴, 𝑅) = pred(𝑧, 𝐴, 𝑅))
10	9	cbviunv 4829	. . . . . 6 ⊢ ∪ 𝑦 ∈ (𝑓‘𝑝) pred(𝑦, 𝐴, 𝑅) = ∪ 𝑧 ∈ (𝑓‘𝑝) pred(𝑧, 𝐴, 𝑅)
11	10	opeq2i 4677	. . . . 5 ⊢ ⟨𝑚, ∪ 𝑦 ∈ (𝑓‘𝑝) pred(𝑦, 𝐴, 𝑅)⟩ = ⟨𝑚, ∪ 𝑧 ∈ (𝑓‘𝑝) pred(𝑧, 𝐴, 𝑅)⟩
12	11	sneqi 4446	. . . 4 ⊢ {⟨𝑚, ∪ 𝑦 ∈ (𝑓‘𝑝) pred(𝑦, 𝐴, 𝑅)⟩} = {⟨𝑚, ∪ 𝑧 ∈ (𝑓‘𝑝) pred(𝑧, 𝐴, 𝑅)⟩}
13	12	uneq2i 4018	. . 3 ⊢ (𝑓 ∪ {⟨𝑚, ∪ 𝑦 ∈ (𝑓‘𝑝) pred(𝑦, 𝐴, 𝑅)⟩}) = (𝑓 ∪ {⟨𝑚, ∪ 𝑧 ∈ (𝑓‘𝑝) pred(𝑧, 𝐴, 𝑅)⟩})
14		dfsbcq 3676	. . 3 ⊢ ((𝑓 ∪ {⟨𝑚, ∪ 𝑦 ∈ (𝑓‘𝑝) pred(𝑦, 𝐴, 𝑅)⟩}) = (𝑓 ∪ {⟨𝑚, ∪ 𝑧 ∈ (𝑓‘𝑝) pred(𝑧, 𝐴, 𝑅)⟩}) → ([(𝑓 ∪ {⟨𝑚, ∪ 𝑦 ∈ (𝑓‘𝑝) pred(𝑦, 𝐴, 𝑅)⟩}) / 𝑓]𝜑 ↔ [(𝑓 ∪ {⟨𝑚, ∪ 𝑧 ∈ (𝑓‘𝑝) pred(𝑧, 𝐴, 𝑅)⟩}) / 𝑓]𝜑))
15	13, 14	ax-mp 5	. 2 ⊢ ([(𝑓 ∪ {⟨𝑚, ∪ 𝑦 ∈ (𝑓‘𝑝) pred(𝑦, 𝐴, 𝑅)⟩}) / 𝑓]𝜑 ↔ [(𝑓 ∪ {⟨𝑚, ∪ 𝑧 ∈ (𝑓‘𝑝) pred(𝑧, 𝐴, 𝑅)⟩}) / 𝑓]𝜑)
16		dfsbcq 3676	. . 3 ⊢ ((𝑓 ∪ {⟨𝑚, ∪ 𝑦 ∈ (𝑓‘𝑝) pred(𝑦, 𝐴, 𝑅)⟩}) = (𝑓 ∪ {⟨𝑚, ∪ 𝑧 ∈ (𝑓‘𝑝) pred(𝑧, 𝐴, 𝑅)⟩}) → ([(𝑓 ∪ {⟨𝑚, ∪ 𝑦 ∈ (𝑓‘𝑝) pred(𝑦, 𝐴, 𝑅)⟩}) / 𝑓]𝜓 ↔ [(𝑓 ∪ {⟨𝑚, ∪ 𝑧 ∈ (𝑓‘𝑝) pred(𝑧, 𝐴, 𝑅)⟩}) / 𝑓]𝜓))
17	13, 16	ax-mp 5	. 2 ⊢ ([(𝑓 ∪ {⟨𝑚, ∪ 𝑦 ∈ (𝑓‘𝑝) pred(𝑦, 𝐴, 𝑅)⟩}) / 𝑓]𝜓 ↔ [(𝑓 ∪ {⟨𝑚, ∪ 𝑧 ∈ (𝑓‘𝑝) pred(𝑧, 𝐴, 𝑅)⟩}) / 𝑓]𝜓)
18		dfsbcq 3676	. . 3 ⊢ ((𝑓 ∪ {⟨𝑚, ∪ 𝑦 ∈ (𝑓‘𝑝) pred(𝑦, 𝐴, 𝑅)⟩}) = (𝑓 ∪ {⟨𝑚, ∪ 𝑧 ∈ (𝑓‘𝑝) pred(𝑧, 𝐴, 𝑅)⟩}) → ([(𝑓 ∪ {⟨𝑚, ∪ 𝑦 ∈ (𝑓‘𝑝) pred(𝑦, 𝐴, 𝑅)⟩}) / 𝑓]𝜒 ↔ [(𝑓 ∪ {⟨𝑚, ∪ 𝑧 ∈ (𝑓‘𝑝) pred(𝑧, 𝐴, 𝑅)⟩}) / 𝑓]𝜒))
19	13, 18	ax-mp 5	. 2 ⊢ ([(𝑓 ∪ {⟨𝑚, ∪ 𝑦 ∈ (𝑓‘𝑝) pred(𝑦, 𝐴, 𝑅)⟩}) / 𝑓]𝜒 ↔ [(𝑓 ∪ {⟨𝑚, ∪ 𝑧 ∈ (𝑓‘𝑝) pred(𝑧, 𝐴, 𝑅)⟩}) / 𝑓]𝜒)
20	13	eqcomi 2780	. 2 ⊢ (𝑓 ∪ {⟨𝑚, ∪ 𝑧 ∈ (𝑓‘𝑝) pred(𝑧, 𝐴, 𝑅)⟩}) = (𝑓 ∪ {⟨𝑚, ∪ 𝑦 ∈ (𝑓‘𝑝) pred(𝑦, 𝐴, 𝑅)⟩})
21		biid 253	. 2 ⊢ ((𝑓 Fn 𝑚 ∧ [𝑚 / 𝑛]𝜑 ∧ [𝑚 / 𝑛]𝜓) ↔ (𝑓 Fn 𝑚 ∧ [𝑚 / 𝑛]𝜑 ∧ [𝑚 / 𝑛]𝜓))
22		biid 253	. 2 ⊢ ((𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ 𝑚) ↔ (𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ 𝑚))
23		biid 253	. 2 ⊢ ((𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ ω ∧ 𝑚 = suc 𝑝) ↔ (𝑚 ∈ 𝐷 ∧ 𝑛 = suc 𝑚 ∧ 𝑝 ∈ ω ∧ 𝑚 = suc 𝑝))
24		biid 253	. 2 ⊢ ((𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ∧ 𝑚 = suc 𝑖) ↔ (𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ∧ 𝑚 = suc 𝑖))
25		biid 253	. 2 ⊢ ((𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ∧ 𝑚 ≠ suc 𝑖) ↔ (𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ∧ 𝑚 ≠ suc 𝑖))
26		eqid 2771	. 2 ⊢ ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)
27		eqid 2771	. 2 ⊢ ∪ 𝑦 ∈ (𝑓‘𝑝) pred(𝑦, 𝐴, 𝑅) = ∪ 𝑦 ∈ (𝑓‘𝑝) pred(𝑦, 𝐴, 𝑅)
28		eqid 2771	. 2 ⊢ ∪ 𝑦 ∈ ((𝑓 ∪ {⟨𝑚, ∪ 𝑧 ∈ (𝑓‘𝑝) pred(𝑧, 𝐴, 𝑅)⟩})‘𝑖) pred(𝑦, 𝐴, 𝑅) = ∪ 𝑦 ∈ ((𝑓 ∪ {⟨𝑚, ∪ 𝑧 ∈ (𝑓‘𝑝) pred(𝑧, 𝐴, 𝑅)⟩})‘𝑖) pred(𝑦, 𝐴, 𝑅)
29		eqid 2771	. 2 ⊢ ∪ 𝑦 ∈ ((𝑓 ∪ {⟨𝑚, ∪ 𝑧 ∈ (𝑓‘𝑝) pred(𝑧, 𝐴, 𝑅)⟩})‘𝑝) pred(𝑦, 𝐴, 𝑅) = ∪ 𝑦 ∈ ((𝑓 ∪ {⟨𝑚, ∪ 𝑧 ∈ (𝑓‘𝑝) pred(𝑧, 𝐴, 𝑅)⟩})‘𝑝) pred(𝑦, 𝐴, 𝑅)
30	1, 2, 3, 4, 5, 6, 7, 8, 15, 17, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 20	bnj600 31870	1 ⊢ (𝑛 ≠ 1o → ((𝑛 ∈ 𝐷 ∧ 𝜃) → 𝜒))

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 387   ∧ w3a 1069   = wceq 1508   ∈ wcel 2051  ∃!weu 2584   ≠ wne 2960  ∀wral 3081  [wsbc 3674   ∖ cdif 3819   ∪ cun 3820  ∅c0 4172  {csn 4435  ⟨cop 4441  ∪ ciun 4788   class class class wbr 4925   E cep 5312  suc csuc 6028   Fn wfn 6180  ‘cfv 6185  ωcom 7394  1_oc1o 7896   ∧ w-bnj17 31636   predc-bnj14 31638   FrSe w-bnj15 31642

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-13 2302  ax-ext 2743  ax-rep 5045  ax-sep 5056  ax-nul 5063  ax-pow 5115  ax-pr 5182  ax-un 7277  ax-reg 8849

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-3or 1070  df-3an 1071  df-tru 1511  df-fal 1521  df-ex 1744  df-nf 1748  df-sb 2017  df-mo 2548  df-eu 2585  df-clab 2752  df-cleq 2764  df-clel 2839  df-nfc 2911  df-ne 2961  df-ral 3086  df-rex 3087  df-reu 3088  df-rab 3090  df-v 3410  df-sbc 3675  df-csb 3780  df-dif 3825  df-un 3827  df-in 3829  df-ss 3836  df-pss 3838  df-nul 4173  df-if 4345  df-pw 4418  df-sn 4436  df-pr 4438  df-tp 4440  df-op 4442  df-uni 4709  df-iun 4790  df-br 4926  df-opab 4988  df-mpt 5005  df-tr 5027  df-id 5308  df-eprel 5313  df-po 5322  df-so 5323  df-fr 5362  df-we 5364  df-xp 5409  df-rel 5410  df-cnv 5411  df-co 5412  df-dm 5413  df-rn 5414  df-res 5415  df-ima 5416  df-ord 6029  df-on 6030  df-lim 6031  df-suc 6032  df-iota 6149  df-fun 6187  df-fn 6188  df-f 6189  df-f1 6190  df-fo 6191  df-f1o 6192  df-fv 6193  df-om 7395  df-1o 7903  df-bnj17 31637  df-bnj14 31639  df-bnj13 31641  df-bnj15 31643

This theorem is referenced by:  bnj852  31872