bnj121 - Mathbox for Jonathan Ben-Naim

	Mathbox for Jonathan Ben-Naim		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > bnj121		Structured version Visualization version GIF version

Theorem bnj121 34495

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)

**Hypotheses**
Ref	Expression
bnj121.1	⊢ (𝜁 ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)))
bnj121.2	⊢ (𝜁′ ↔ [1_o / 𝑛]𝜁)
bnj121.3	⊢ (𝜑′ ↔ [1_o / 𝑛]𝜑)
bnj121.4	⊢ (𝜓′ ↔ [1_o / 𝑛]𝜓)

**Assertion**
Ref	Expression
bnj121	⊢ (𝜁′ ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑓 Fn 1_o ∧ 𝜑′ ∧ 𝜓′)))

Distinct variable groups: 𝐴,𝑛 𝑅,𝑛 𝑓,𝑛 𝑥,𝑛 Allowed substitution hints: 𝜑(𝑥,𝑓,𝑛) 𝜓(𝑥,𝑓,𝑛) 𝜁(𝑥,𝑓,𝑛) 𝐴(𝑥,𝑓) 𝑅(𝑥,𝑓) 𝜑′(𝑥,𝑓,𝑛) 𝜓′(𝑥,𝑓,𝑛) 𝜁′(𝑥,𝑓,𝑛)

**Proof of Theorem bnj121**
Step	Hyp	Ref	Expression
1		bnj121.1	. . 3 ⊢ (𝜁 ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)))
2	1	sbcbii 3835	. 2 ⊢ ([1_o / 𝑛]𝜁 ↔ [1_o / 𝑛]((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)))
3		bnj121.2	. 2 ⊢ (𝜁′ ↔ [1_o / 𝑛]𝜁)
4		bnj105 34349	. . . . . . . 8 ⊢ 1_o ∈ V
5	4	bnj90 34347	. . . . . . 7 ⊢ ([1_o / 𝑛]𝑓 Fn 𝑛 ↔ 𝑓 Fn 1_o)
6	5	bicomi 223	. . . . . 6 ⊢ (𝑓 Fn 1_o ↔ [1_o / 𝑛]𝑓 Fn 𝑛)
7		bnj121.3	. . . . . 6 ⊢ (𝜑′ ↔ [1_o / 𝑛]𝜑)
8		bnj121.4	. . . . . 6 ⊢ (𝜓′ ↔ [1_o / 𝑛]𝜓)
9	6, 7, 8	3anbi123i 1153	. . . . 5 ⊢ ((𝑓 Fn 1_o ∧ 𝜑′ ∧ 𝜓′) ↔ ([1_o / 𝑛]𝑓 Fn 𝑛 ∧ [1_o / 𝑛]𝜑 ∧ [1_o / 𝑛]𝜓))
10		sbc3an 3844	. . . . 5 ⊢ ([1_o / 𝑛](𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓) ↔ ([1_o / 𝑛]𝑓 Fn 𝑛 ∧ [1_o / 𝑛]𝜑 ∧ [1_o / 𝑛]𝜓))
11	9, 10	bitr4i 278	. . . 4 ⊢ ((𝑓 Fn 1_o ∧ 𝜑′ ∧ 𝜓′) ↔ [1_o / 𝑛](𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))
12	11	imbi2i 336	. . 3 ⊢ (((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑓 Fn 1_o ∧ 𝜑′ ∧ 𝜓′)) ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → [1_o / 𝑛](𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)))
13		nfv 1910	. . . . 5 ⊢ Ⅎ𝑛(𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴)
14	13	sbc19.21g 3852	. . . 4 ⊢ (1_o ∈ V → ([1_o / 𝑛]((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)) ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → [1_o / 𝑛](𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓))))
15	4, 14	ax-mp 5	. . 3 ⊢ ([1_o / 𝑛]((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)) ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → [1_o / 𝑛](𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)))
16	12, 15	bitr4i 278	. 2 ⊢ (((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑓 Fn 1_o ∧ 𝜑′ ∧ 𝜓′)) ↔ [1_o / 𝑛]((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)))
17	2, 3, 16	3bitr4i 303	1 ⊢ (𝜁′ ↔ ((𝑅 FrSe 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑓 Fn 1_o ∧ 𝜑′ ∧ 𝜓′)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 395 ∧ w3a 1085 ∈ wcel 2099 Vcvv 3470 [wsbc 3775 Fn wfn 6537 1_oc1o 8473 FrSe w-bnj15 34317

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-10 2130 ax-12 2167 ax-ext 2699 ax-sep 5293 ax-nul 5300 ax-pow 5359

This theorem depends on definitions: df-bi 206 df-an 396 df-or 847 df-3an 1087 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2061 df-clab 2706 df-cleq 2720 df-clel 2806 df-v 3472 df-sbc 3776 df-dif 3948 df-un 3950 df-in 3952 df-ss 3962 df-nul 4319 df-pw 4600 df-sn 4625 df-suc 6369 df-fn 6545 df-1o 8480

This theorem is referenced by: bnj150 34501 bnj153 34505

W3C validator

	
		OSZAR »